1 /-
2 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Johannes Hölzl, Johan Commelin, Mario Carneiro
5 -/
6
7 import algebra.ring
src └──────────┘
8 import data.finsupp data.polynomial data.equiv.algebra
src └──────────┘ └─────────────┘ └────────────────┘
9
10 /-!
11 # Multivariate polynomials
12
13 This file defines polynomial rings over a base ring (or even semiring),
14 with variables from a general type `σ` (which could be infinite).
15
16 ## Important definitions
17
18 Let `R` be a commutative ring (or a semiring) and let `σ` be an arbitrary
19 type. This file creates the type `mv_polynomial σ R`, which mathematicians
20 might denote `R[X_i : i ∈ σ]`. It is the type of multivariate
21 (a.k.a. multivariable) polynomials, with variables
22 corresponding to the terms in `σ`, and coefficients in `R`.
23
24 ### Notation
25
26 In the definitions below, we use the following notation:
27
28 + `σ : Type*` (indexing the variables)
29
30 + `R : Type*` `[comm_semiring R]` (the coefficients)
31
32 + `s : σ →₀ ℕ`, a function from `σ` to `ℕ` which is zero away from a finite set.
33 This will give rise to a monomial in `mv_polynomial σ R` which mathematicians might call `X^s`
34
35 + `a : R`
36
37 + `i : σ`, with corresponding monomial `X i`, often denoted `X_i` by mathematicians
38
39 + `p : mv_polynomial σ R`
40
41 ### Definitions
42
43 * `mv_polynomial σ R` : the type of polynomials with variables of type `σ` and coefficients
44 in the commutative semiring `R`
45
46 * `monomial s a` : the monomial which mathematically would be denoted `a * X^s`
47
48 * `C a` : the constant polynomial with value `a`
49
50 * `X i` : the degree one monomial corresponding to i; mathematically this might be denoted `Xᵢ`.
51
52 * `coeff s p` : the coefficient of `s` in `p`.
53
54 * `eval₂ (f : R → S) (g : σ → S) p` : given a semiring homomorphism from `R` to another
55 semiring `S`, and a map `σ → S`, evaluates `p` at this valuation, returning a term of type `S`.
56 Note that `eval₂` can be made using `eval` and `map` (see below), and it has been suggested
57 that sticking to `eval` and `map` might make the code less brittle.
58
59 * `eval (g : σ → R) p` : given a map `σ → R`, evaluates `p` at this valuation,
60 returning a term of type `R`
61
62 * `map (f : R → S) p` : returns the multivariate polynomial obtained from `p` by the change of
63 coefficient semiring corresponding to `f`
64
65 * `degrees p` : the multiset of variables representing the union of the multisets corresponding
66 to each non-zero monomial in `p`. For example if `7 ≠ 0` in `R` and `p = x²y+7y³` then
67 `degrees p = {x, x, y, y, y}`
68
69 * `vars p` : the finset of variables occurring in `p`. For example if `p = x⁴y+yz` then
70 `vars p = {x, y, z}`
71
72 * `degree_of n p : ℕ` -- the total degree of `p` with respect to the variable `n`. For example
73 if `p = x⁴y+yz` then `degree_of y p = 1`.
74
75 * `total_degree p : ℕ` -- the max of the sizes of the multisets `s` whose monomials `X^s` occur
76 in `p`. For example if `p = x⁴y+yz` then `total_degree p = 5`.
77
78 ## Implementation notes
79
80 Recall that if `Y` has a zero, then `X →₀ Y` is the type of functions from `X` to `Y` with finite
81 support, i.e. such that only finitely many elements of `X` get sent to non-zero terms in `Y`.
82 The definition of `mv_polynomial σ α` is `(σ →₀ ℕ) →₀ α` ; here `σ →₀ ℕ` denotes the space of all
83 monomials in the variables, and the function to α sends a monomial to its coefficient in
84 the polynomial being represented.
85
86 ## Tags
87
88 polynomial, multivariate polynomial, multivariable polynomial
89 -/
90
91 noncomputable theory
92 local attribute [instance, priority 100] classical.prop_decidable
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
93
94 open set function finsupp lattice
95
96 universes u v w x
97 variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x}
98
99 /-- Multivariate polynomial, where `σ` is the index set of the variables and
100 `α` is the coefficient ring -/
101 def mv_polynomial (σ : Type*) (α : Type*) [comm_semiring α] := (σ →₀ ℕ) →₀ α
id └───────────┘ ┴ ┴ └┘ ┴ └┘ ┴
src └───────────┘ └┘ ┴ └┘
typ └───────────┘ ┴ ┴ └┘ ┴ └┘ ┴
doc └┘ └┘
102
103 namespace mv_polynomial
104 variables {σ : Type*} {a a' a₁ a₂ : α} {e : ℕ} {n m : σ} {s : σ →₀ ℕ}
id ┴ └┘ ┴
src ┴ └┘ ┴
typ ┴ └┘ ┴
doc └┘
st └┘
105
106 section comm_semiring
107 variables [comm_semiring α] {p q : mv_polynomial σ α}
id └───────────┘ └───────────┘
src └───────────┘ └───────────┘
typ └───────────┘ └───────────┘
doc └───────────┘
108
109 instance decidable_eq_mv_polynomial [decidable_eq σ] [decidable_eq α] :
id └──────────┘ ┴ └──────────┘ ┴
src └──────────┘ └──────────┘
typ └──────────┘ ┴ └──────────┘ ┴
110 decidable_eq (mv_polynomial σ α) := finsupp.decidable_eq
id └──────────┘ └───────────┘ ┴ ┴ └──────────────────┘
src └──────────┘ └───────────┘ └──────────────────┘
typ └──────────┘ └───────────┘ ┴ ┴ └──────────────────┘
doc └───────────┘
111 instance : has_zero (mv_polynomial σ α) := finsupp.has_zero
id └──────┘ └───────────┘ ┴ ┴ └──────────────┘
src └──────┘ └───────────┘ └──────────────┘
typ └──────┘ └───────────┘ ┴ ┴ └──────────────┘
doc └───────────┘
112 instance : has_one (mv_polynomial σ α) := finsupp.has_one
id └─────┘ └───────────┘ ┴ ┴ └─────────────┘
src └─────┘ └───────────┘ └─────────────┘
typ └─────┘ └───────────┘ ┴ ┴ └─────────────┘
doc └───────────┘ └─────────────┘
113 instance : has_add (mv_polynomial σ α) := finsupp.has_add
id └─────┘ └───────────┘ ┴ ┴ └─────────────┘
src └─────┘ └───────────┘ └─────────────┘
typ └─────┘ └───────────┘ ┴ ┴ └─────────────┘
doc └───────────┘
114 instance : has_mul (mv_polynomial σ α) := finsupp.has_mul
id └─────┘ └───────────┘ ┴ ┴ └─────────────┘
src └─────┘ └───────────┘ └─────────────┘
typ └─────┘ └───────────┘ ┴ ┴ └─────────────┘
doc └───────────┘ └─────────────┘
115 instance : comm_semiring (mv_polynomial σ α) := finsupp.comm_semiring
id └───────────┘ └───────────┘ ┴ ┴ └───────────────────┘
src └───────────┘ └───────────┘ └───────────────────┘
typ └───────────┘ └───────────┘ ┴ ┴ └───────────────────┘
doc └───────────┘
116 instance : inhabited (mv_polynomial σ α) := ⟨0⟩
id └───────┘ └───────────┘ ┴ ┴
src └───────┘ └───────────┘
typ └───────┘ └───────────┘ ┴ ┴
doc └───────────┘
117
118 /-- `monomial s a` is the monomial `a * X^s` -/
119 def monomial (s : σ →₀ ℕ) (a : α) : mv_polynomial σ α := single s a
id ┴ └┘ ┴ ┴ └───────────┘ ┴ ┴ └────┘ ┴ ┴
src └┘ ┴ └───────────┘ └────┘
typ ┴ └┘ ┴ ┴ └───────────┘ ┴ ┴ └────┘ ┴ ┴
doc └┘ └───────────┘ └────┘
120
121 /-- `C a` is the constant polynomial with value `a` -/
122 def C (a : α) : mv_polynomial σ α := monomial 0 a
id ┴ └───────────┘ ┴ ┴ └──────┘ ┴
src └───────────┘ └──────┘
typ ┴ └───────────┘ ┴ ┴ └──────┘ ┴
doc └───────────┘ └──────┘
123
124 /-- `X n` is the degree `1` monomial `1*n` -/
125 def X (n : σ) : mv_polynomial σ α := monomial (single n 1) 1
id ┴ └───────────┘ ┴ ┴ └──────┘ └────┘ ┴
src └───────────┘ └──────┘ └────┘
typ ┴ └───────────┘ ┴ ┴ └──────┘ └────┘ ┴
doc └───────────┘ └──────┘ └────┘
126
127 @[simp] lemma C_0 : C 0 = (0 : mv_polynomial σ α) := by simp [C, monomial]; refl
id ┴ ┴ └───────────┘ ┴ ┴ ┴ └──────┘
src ┴ ┴ └───────────┘ └────┘┴└┘└──────┘┴ └────
typ ┴ ┴ └───────────┘ ┴ ┴ └────┘┴└┘└──────┘┴ └────
doc └──┘ ┴ └───────────┘ └────┘┴└┘└──────┘┴ └────
txt └────┘ └┘ ┴ └────
par └────┘ └┘ ┴ └────
pid ┴┴ └┘ ┴ └
st └─────────────────────────
128
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
129 @[simp] lemma C_1 : C 1 = (1 : mv_polynomial σ α) := rfl
id ┴ ┴ └───────────┘ ┴ ┴ └─┘
src ┴ ┴ └───────────┘ └─┘
typ ┴ ┴ └───────────┘ ┴ ┴ └─┘
doc └──┘ ┴ └───────────┘
130
131 lemma C_mul_monomial : C a * monomial s a' = monomial s (a * a') :=
id ┴ ┴ ┴ └──────┘ ┴ └┘ ┴ └──────┘ ┴ ┴ ┴ └┘
src ┴ ┴ └──────┘ ┴ └──────┘ ┴
typ ┴ ┴ ┴ └──────┘ ┴ └┘ ┴ └──────┘ ┴ ┴ ┴ └┘
doc ┴ └──────┘ └──────┘
132 by simp [C, monomial, single_mul_single]
id ┴ └──────┘ └───────────────┘
src └────┘┴└┘└──────┘└┘└───────────────┘└─
typ └────┘┴└┘└──────┘└┘└───────────────┘└─
doc └────┘┴└┘└──────┘└┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
st └──────────────────────────────────────
133
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
134 @[simp] lemma C_add : (C (a + a') : mv_polynomial σ α) = C a + C a' := single_add
id ┴ ┴ ┴ └┘ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └────────┘
src ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ └────────┘
typ ┴ ┴ ┴ └┘ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └────────┘
doc └──┘ ┴ └───────────┘ ┴ ┴
135
136 @[simp] lemma C_mul : (C (a * a') : mv_polynomial σ α) = C a * C a' := C_mul_monomial.symm
id ┴ ┴ ┴ └┘ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └────────────┘└───┘
src ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ └────────────┘└───┘
typ ┴ ┴ ┴ └┘ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └────────────┘└───┘
doc └──┘ ┴ └───────────┘ ┴ ┴
137
138 @[simp] lemma C_pow (a : α) (n : ℕ) : (C (a^n) : mv_polynomial σ α) = (C a)^n :=
id ┴ ┴ ┴ ┴┴┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴┴
src ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴┴
doc └──┘ ┴ └───────────┘ ┴
139 by induction n; simp [pow_succ, *]
id ┴ └──────┘
src └────────┘ └────┘└──────┘└────
typ └────────┘┴ └────┘└──────┘└────
doc └────────┘ └────┘ └────
txt └────────┘ └────┘ └────
par └────────┘ └────┘ └────
pid ┴ ┴┴ └──┘└
st └────────────────────────────────
140
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
141 instance : is_semiring_hom (C : α → mv_polynomial σ α) :=
id └─────────────┘ ┴ ┴ └───────────┘ ┴ ┴
src └─────────────┘ ┴ └───────────┘
typ └─────────────┘ ┴ ┴ └───────────┘ ┴ ┴
doc └─────────────┘ ┴ └───────────┘
142 { map_zero := C_0,
id └─┘
src └─┘
typ └─┘
143 map_one := C_1,
id └─┘
src └─┘
typ └─┘
144 map_add := λ a a', C_add,
id ┴ └┘ └───┘
src └───┘
typ ┴ └┘ └───┘
145 map_mul := λ a a', C_mul }
id ┴ └┘ └───┘
src └───┘
typ ┴ └┘ └───┘
146
147 lemma C_eq_coe_nat (n : ℕ) : (C ↑n : mv_polynomial σ α) = n :=
id ┴ ┴ ┴┴ └───────────┘ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ └───────────┘ ┴
typ ┴ ┴ ┴┴ └───────────┘ ┴ ┴ ┴ ┴
doc ┴ └───────────┘
148 by induction n; simp [nat.succ_eq_add_one, *]
id ┴ └─────────────────┘
src └────────┘ └────┘└─────────────────┘└────
typ └────────┘┴ └────┘└─────────────────┘└────
doc └────────┘ └────┘ └────
txt └────────┘ └────┘ └────
par └────────┘ └────┘ └────
pid ┴ ┴┴ └──┘└
st └───────────────────────────────────────────
149
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
150 lemma X_pow_eq_single : X n ^ e = monomial (single n e) (1 : α) :=
id ┴ ┴ ┴ ┴ ┴ └──────┘ └────┘ ┴ ┴ ┴
src ┴ ┴ ┴ └──────┘ └────┘
typ ┴ ┴ ┴ ┴ ┴ └──────┘ └────┘ ┴ ┴ ┴
doc ┴ └──────┘ └────┘
151 begin
st └─────
152 induction e,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ────────────┘└─
153 { simp [X], refl },
id ┴
src └────┘┴┴ └───┘
typ └────┘┴┴ └───┘
doc └────┘┴┴ └───┘
txt └────┘ ┴ └───┘
par └────┘ ┴ └───┘
pid ┴┴ ┴ ┴
st ───┘└──────┘└─────┘└┘└
154 { simp [pow_succ, e_ih],
id └──────┘ └──┘
src └────┘└──────┘└┘ ┴
typ └────┘└──────┘└┘└──┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st ────────────────────────┘└─
155 simp [X, monomial, single_mul_single, nat.succ_eq_add_one] }
id ┴ └──────┘ └───────────────┘ └─────────────────┘
src └────┘┴└┘└──────┘└┘└───────────────┘└┘└─────────────────┘└┘
typ └────┘┴└┘└──────┘└┘└───────────────┘└┘└─────────────────┘└┘
doc └────┘┴└┘└──────┘└┘ └┘ └┘
txt └────┘ └┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘ └┘
pid ┴┴ └┘ └┘ └┘ ┴┴
st ──────────────────────────────────────────────────────────────┘└─
156 end
st ──┘
157
158 lemma monomial_add_single : monomial (s + single n e) a = (monomial s a * X n ^ e) :=
id └──────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ └────┘ ┴ └──────┘ ┴ ┴ ┴
typ └──────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────┘ └────┘ └──────┘ ┴
159 by rw [X_pow_eq_single, monomial, monomial, monomial, single_mul_single]; simp
id └─────────────┘ └──────┘ └──────┘ └──────┘ └───────────────┘
src └──┘└─────────────┘└┘└──────┘└┘└──────┘└┘└──────┘└┘└───────────────┘┴ └────
typ └──┘└─────────────┘└┘└──────┘└┘└──────┘└┘└──────┘└┘└───────────────┘┴ └────
doc └──┘ └┘└──────┘└┘└──────┘└┘└──────┘└┘ ┴ └────
txt └──┘ └┘ └┘ └┘ └┘ ┴ └────
par └──┘ └┘ └┘ └┘ └┘ ┴ └────
pid └┘ └┘ └┘ └┘ └┘ ┴ └
st └──────────────────┘└────────┘└────────┘└────────┘└─────────────────┘┴└──────
160
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
161 lemma monomial_single_add : monomial (single n e + s) a = (X n ^ e * monomial s a) :=
id └──────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴
src └──────┘ └────┘ ┴ ┴ ┴ ┴ ┴ └──────┘
typ └──────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴
doc └──────┘ └────┘ ┴ └──────┘
162 by rw [X_pow_eq_single, monomial, monomial, monomial, single_mul_single]; simp
id └─────────────┘ └──────┘ └──────┘ └──────┘ └───────────────┘
src └──┘└─────────────┘└┘└──────┘└┘└──────┘└┘└──────┘└┘└───────────────┘┴ └────
typ └──┘└─────────────┘└┘└──────┘└┘└──────┘└┘└──────┘└┘└───────────────┘┴ └────
doc └──┘ └┘└──────┘└┘└──────┘└┘└──────┘└┘ ┴ └────
txt └──┘ └┘ └┘ └┘ └┘ ┴ └────
par └──┘ └┘ └┘ └┘ └┘ ┴ └────
pid └┘ └┘ └┘ └┘ └┘ ┴ └
st └──────────────────┘└────────┘└────────┘└────────┘└─────────────────┘┴└──────
163
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
164 lemma monomial_eq : monomial s a = C a * (s.prod $ λn e, X n ^ e : mv_polynomial σ α) :=
id └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴
src └──────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └───────────┘
typ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴
doc └──────┘ ┴ └───┘ ┴ └───────────┘
165 begin
st └─────
166 apply @finsupp.induction σ ℕ _ _ s,
id └───────────────┘ ┴ ┴
src └────┘ └───────────────┘┴ ┴ └───┘
typ └────┘ └───────────────┘┴┴┴ └───┘┴
doc └────┘ ┴ ┴ └───┘
txt └────┘ ┴ ┴ └───┘
par └────┘ ┴ ┴ └───┘
pid ┴ ┴ ┴ └───┘
st ───────────────────────────────────┘└─
167 { simp [C, prod_zero_index]; exact (mul_one _).symm },
id ┴ └─────────────┘
src └────┘┴└┘└─────────────┘┴ └────┘ └───────┘
typ └────┘┴└┘└─────────────┘┴ └────┘ └───────┘
doc └────┘┴└┘ ┴ └────┘ └───────┘
txt └────┘ └┘ ┴ └────┘ └───────┘
par └────┘ └┘ ┴ └────┘ └───────┘
pid ┴┴ └┘ ┴ ┴ └─────┘└┘
st ───┘└────────────────────────────────────────────────┘└┘└
168 { assume n e s hns he ih,
src └────────────────────┘
typ └────────────────────┘
doc └────────────────────┘
txt └────────────────────┘
par └────────────────────┘
pid └────────────────────┘
st ─────────────────────────┘└─
169 simp [prod_add_index, prod_single_index, pow_zero, pow_add, (mul_assoc _ _ _).symm, ih.symm,
id └────────────┘ └───────────────┘ └──────┘ └─────┘ └───────┘
src └────┘└────────────┘└┘└───────────────┘└┘└──────┘└┘└─────┘└┘ └───────┘└────────────┘ └─
typ └────┘└────────────┘└┘└───────────────┘└┘└──────┘└┘└─────┘└┘ └───────┘└────────────┘└─────┘└─
doc └────┘ └┘ └┘ └┘ └┘ └────────────┘ └─
txt └────┘ └┘ └┘ └┘ └┘ └────────────┘ └─
par └────┘ └┘ └┘ └┘ └┘ └────────────┘ └─
pid ┴┴ └┘ └┘ └┘ └┘ └────────────┘ └─
st ─────────────────────────────────────────────────────────────────────────────────────────────────
170 monomial_add_single] }
id └─────────────────┘
src ─────┘└─────────────────┘└┘
typ ─────┘└─────────────────┘└┘
doc ─────┘ └┘
txt ─────┘ └┘
par ─────┘ └┘
pid ─────┘ ┴┴
st ──────────────────────────┘└─
171 end
st ──┘
172
173 @[recursor 5]
doc └──────┘
174 lemma induction_on {M : mv_polynomial σ α → Prop} (p : mv_polynomial σ α)
id └───────────┘ ┴ ┴ └───────────┘ ┴ ┴
src └───────────┘ └───────────┘
typ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴
doc └───────────┘ └───────────┘
175 (h_C : ∀a, M (C a)) (h_add : ∀p q, M p → M q → M (p + q)) (h_X : ∀p n, M p → M (p * X n)) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴
176 M p :=
id ┴ ┴
typ ┴ ┴
177 have ∀s a, M (monomial s a),
id ┴ ┴ ┴ └──────┘ ┴ ┴
src └──────┘
typ ┴ ┴ ┴ └──────┘ ┴ ┴
doc └──────┘
178 begin
st └─────
179 assume s a,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └────────┘
st ───────────┘└─
180 apply @finsupp.induction σ ℕ _ _ s,
id └───────────────┘ ┴ ┴
src └────┘ └───────────────┘┴ ┴ └───┘
typ └────┘ └───────────────┘┴┴┴ └───┘┴
doc └────┘ ┴ ┴ └───┘
txt └────┘ ┴ ┴ └───┘
par └────┘ ┴ ┴ └───┘
pid ┴ ┴ ┴ └───┘
st ───────────────────────────────────┘└─
181 { show M (monomial 0 a), from h_C a, },
id ┴ └──────┘ ┴ └─┘ ┴
src └───┘ ┴ └──────┘└─┘ ┴ └───┘ ┴
typ └───┘┴┴ └──────┘└─┘┴┴ └───┘└─┘┴┴
doc └───┘ ┴ └──────┘└─┘ ┴ └───┘ ┴
txt └───┘ ┴ └─┘ ┴ └───┘ ┴
par └───┘ ┴ └─┘ ┴ └───┘ ┴
pid └───┘ ┴ └─┘ ┴ └───┘ ┴
st ───┘└───────────────────┘└──────────┘└──┘└
182 { assume n e p hpn he ih,
src └────────────────────┘
typ └────────────────────┘
doc └────────────────────┘
txt └────────────────────┘
par └────────────────────┘
pid └────────────────────┘
st ─────────────────────────┘└─
183 have : ∀e:ℕ, M (monomial p a * X n ^ e),
id ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └┘ ┴ ┴ └──────┘┴ ┴ ┴┴┴┴┴ ┴┴┴ ┴
typ └─────┘ └┘ ┴┴┴ └──────┘┴┴┴┴┴┴┴┴┴┴┴┴┴ ┴
doc └─────┘ └┘ ┴ ┴ └──────┘┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
txt └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────┘└─
184 { intro e,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ─────┘└─────┘└─
185 induction e,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ────────────────┘└─
186 { simp [ih] },
id └┘
src └────┘ └┘
typ └────┘└┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ───────┘└────────┘└┘└
187 { simp [ih, pow_succ', (mul_assoc _ _ _).symm, h_X, e_ih] } },
id └┘ └───────┘ └───────┘ └─┘ └──┘
src └────┘ └┘└───────┘└┘ └───────┘└────────────┘ └┘ └┘
typ └────┘└┘└┘└───────┘└┘ └───────┘└────────────┘└─┘└┘└──┘└┘
doc └────┘ └┘ └┘ └────────────┘ └┘ └┘
txt └────┘ └┘ └┘ └────────────┘ └┘ └┘
par └────┘ └┘ └┘ └────────────┘ └┘ └┘
pid ┴┴ └┘ └┘ └────────────┘ └┘ ┴┴
st ───────────────────────────────────────────────────────────────┘└──┘└
188 simp [monomial_add_single, this] }
id └─────────────────┘ └──┘
src └────┘└─────────────────┘└┘ └┘
typ └────┘└─────────────────┘└┘└──┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ────────────────────────────────────┘└─
189 end,
st ──┘
190 finsupp.induction p
id └───────────────┘ ┴
src └───────────────┘
typ └───────────────┘ ┴
191 (by have : M (C 0) := h_C 0; rwa [C_0] at this)
id ┴ ┴ └─┘ └─┘
src └─────┘ ┴ ┴└─────┘ └┘ └───┘└─┘└───────┘
typ └─────┘┴┴ ┴└─────┘└─┘└┘ └───┘└─┘└───────┘
doc └─────┘ ┴ ┴└─────┘ └┘ └───┘ └───────┘
txt └─────┘ ┴ └─────┘ └┘ └───┘ └───────┘
par └─────┘ ┴ └─────┘ └┘ └───┘ └───────┘
pid └───┘└┘ ┴ └─┘└──┘ ┴┴ └┘ ┴└──────┘
st └─────────────────────────────┘└─┘┴└──────┘
192 (assume s a p hsp ha hp, h_add _ _ (this s a) hp)
id ┴ ┴ ┴ └─┘ └┘ └┘ └───┘ └──┘ ┴ ┴ └┘
typ ┴ ┴ ┴ └─┘ └┘ └┘ └───┘ └──┘ ┴ ┴ └┘
193
194 lemma hom_eq_hom [semiring γ]
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
195 (f g : mv_polynomial σ α → γ) (hf : is_semiring_hom f) (hg : is_semiring_hom g)
id └───────────┘ ┴ ┴ ┴ └─────────────┘ ┴ └─────────────┘ ┴
src └───────────┘ └─────────────┘ └─────────────┘
typ └───────────┘ ┴ ┴ ┴ └─────────────┘ ┴ └─────────────┘ ┴
doc └───────────┘ └─────────────┘ └─────────────┘
196 (hC : ∀a:α, f (C a) = g (C a)) (hX : ∀n:σ, f (X n) = g (X n)) (p : mv_polynomial σ α) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴
doc ┴ ┴ ┴ ┴ └───────────┘
197 f p = g p :=
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
198 mv_polynomial.induction_on p hC
id └────────────────────────┘ ┴ └┘
src └────────────────────────┘
typ └────────────────────────┘ ┴ └┘
199 begin assume p q hp hq, rw [is_semiring_hom.map_add f, is_semiring_hom.map_add g, hp, hq] end
id └─────────────────────┘ ┴ └─────────────────────┘ ┴ └┘ └┘
src └──────────────┘ └──┘└─────────────────────┘┴ └┘└─────────────────────┘┴ └┘ └┘ └┘
typ └──────────────┘ └──┘└─────────────────────┘┴┴└┘└─────────────────────┘┴┴└┘└┘└┘└┘└┘
doc └──────────────┘ └──┘ ┴ └┘ ┴ └┘ └┘ └┘
txt └──────────────┘ └──┘ ┴ └┘ ┴ └┘ └┘ └┘
par └──────────────┘ └──┘ ┴ └┘ ┴ └┘ └┘ └┘
pid └──────────────┘ └┘ ┴ └┘ ┴ └┘ └┘ ┴┴
st └────────────────────┘└─────────────────────────────┘└─────────────────────────┘└──┘└──┘┴┴└─┘
200 begin assume p n hp, rw [is_semiring_hom.map_mul f, is_semiring_hom.map_mul g, hp, hX] end
id └─────────────────────┘ ┴ └─────────────────────┘ ┴ └┘ └┘
src └───────────┘ └──┘└─────────────────────┘┴ └┘└─────────────────────┘┴ └┘ └┘ └┘
typ └───────────┘ └──┘└─────────────────────┘┴┴└┘└─────────────────────┘┴┴└┘└┘└┘└┘└┘
doc └───────────┘ └──┘ ┴ └┘ ┴ └┘ └┘ └┘
txt └───────────┘ └──┘ ┴ └┘ ┴ └┘ └┘ └┘
par └───────────┘ └──┘ ┴ └┘ ┴ └┘ └┘ └┘
pid └───────────┘ └┘ ┴ └┘ ┴ └┘ └┘ ┴┴
st └─────────────────┘└─────────────────────────────┘└─────────────────────────┘└──┘└──┘┴┴└─┘
201
202 lemma is_id (f : mv_polynomial σ α → mv_polynomial σ α) (hf : is_semiring_hom f)
id └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ └─────────────┘ ┴
src └───────────┘ └───────────┘ └─────────────┘
typ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ └─────────────┘ ┴
doc └───────────┘ └───────────┘ └─────────────┘
203 (hC : ∀a:α, f (C a) = (C a)) (hX : ∀n:σ, f (X n) = (X n)) (p : mv_polynomial σ α) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴
doc ┴ ┴ ┴ ┴ └───────────┘
204 f p = p :=
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
205 hom_eq_hom f id hf is_semiring_hom.id hC hX p
id └────────┘ ┴ └┘ └┘ └────────────────┘ └┘ └┘ ┴
src └────────┘ └┘ └────────────────┘
typ └────────┘ ┴ └┘ └┘ └────────────────┘ └┘ └┘ ┴
doc └────────────────┘
206
207 section coeff
208
209 section
210 -- While setting up `coeff`, we make `mv_polynomial` reducible so we can treat it as a function.
211 local attribute [reducible] mv_polynomial
id └───────────┘
src └───────────┘
typ └───────────┘
doc └───────┘ └───────────┘
212
213 /-- The coefficient of the monomial `m` in the multi-variable polynomial `p`. -/
214 def coeff (m : σ →₀ ℕ) (p : mv_polynomial σ α) : α := p m
id ┴ └┘ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ └───────────┘
typ ┴ └┘ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
doc └┘ └───────────┘
215 end
216
217 lemma ext (p q : mv_polynomial σ α) :
id └───────────┘ ┴ ┴
src └───────────┘
typ └───────────┘ ┴ ┴
doc └───────────┘
218 (∀ m, coeff m p = coeff m q) → p = q := ext
id ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └─┘
src └───┘ ┴ └───┘ ┴ └─┘
typ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └─┘
doc └───┘ └───┘
219
220 lemma ext_iff (p q : mv_polynomial σ α) :
id └───────────┘ ┴ ┴
src └───────────┘
typ └───────────┘ ┴ ┴
doc └───────────┘
221 (∀ m, coeff m p = coeff m q) ↔ p = q :=
id ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ └───┘ ┴ ┴
typ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ └───┘
222 ⟨ext p q, λ h m, by rw h⟩
id └─┘ ┴ ┴ ┴ ┴ ┴
src └─┘ └─┘
typ └─┘ ┴ ┴ ┴ ┴ └─┘┴
doc └─┘
txt └─┘
par └─┘
pid ┴
st └───┘
223
224 @[simp] lemma coeff_add (m : σ →₀ ℕ) (p q : mv_polynomial σ α) :
id ┴ └┘ ┴ └───────────┘ ┴ ┴
src └┘ ┴ └───────────┘
typ ┴ └┘ ┴ └───────────┘ ┴ ┴
doc └──┘ └┘ └───────────┘
225 coeff m (p + q) = coeff m p + coeff m q := add_apply
id └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ └───────┘
src └───┘ ┴ ┴ └───┘ ┴ └───┘ └───────┘
typ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ └───────┘
doc └───┘ └───┘ └───┘
226
227 @[simp] lemma coeff_zero (m : σ →₀ ℕ) :
id ┴ └┘ ┴
src └┘ ┴
typ ┴ └┘ ┴
doc └──┘ └┘
228 coeff m (0 : mv_polynomial σ α) = 0 := rfl
id └───┘ ┴ └───────────┘ ┴ ┴ ┴ └─┘
src └───┘ └───────────┘ ┴ └─┘
typ └───┘ ┴ └───────────┘ ┴ ┴ ┴ └─┘
doc └───┘ └───────────┘
229
230 @[simp] lemma coeff_zero_X (i : σ) : coeff 0 (X i : mv_polynomial σ α) = 0 :=
id ┴ └───┘ ┴ ┴ └───────────┘ ┴ ┴ ┴
src └───┘ ┴ └───────────┘ ┴
typ ┴ └───┘ ┴ ┴ └───────────┘ ┴ ┴ ┴
doc └──┘ └───┘ ┴ └───────────┘
231 single_eq_of_ne (λ h, by cases single_eq_zero.1 h)
id └─────────────┘ ┴ └────────────┘ ┴
src └─────────────┘ └────┘└────────────┘└─┘
typ └─────────────┘ ┴ └────┘└────────────┘└─┘┴
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st └───────────────────────┘
232
233 instance coeff.is_add_monoid_hom (m : σ →₀ ℕ) :
id ┴ └┘ ┴
src └┘ ┴
typ ┴ └┘ ┴
doc └┘
234 is_add_monoid_hom (coeff m : mv_polynomial σ α → α) :=
id └───────────────┘ └───┘ ┴ └───────────┘ ┴ ┴ ┴
src └───────────────┘ └───┘ └───────────┘
typ └───────────────┘ └───┘ ┴ └───────────┘ ┴ ┴ ┴
doc └───────────────┘ └───┘ └───────────┘
235 { map_add := coeff_add m,
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
236 map_zero := coeff_zero m }
id └────────┘ ┴
src └────────┘
typ └────────┘ ┴
237
238 lemma coeff_sum {X : Type*} (s : finset X) (f : X → mv_polynomial σ α) (m : σ →₀ ℕ) :
id └────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ └┘ ┴
src └────┘ └───────────┘ └┘ ┴
typ └────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ └┘ ┴
doc └────┘ └───────────┘ └┘
239 coeff m (s.sum f) = s.sum (λ x, coeff m (f x)) :=
id └───┘ ┴ ┴└──┘ ┴ ┴ ┴└──┘ ┴ └───┘ ┴ ┴ ┴
src └───┘ └──┘ ┴ └──┘ └───┘
typ └───┘ ┴ ┴└──┘ ┴ ┴ ┴└──┘ ┴ └───┘ ┴ ┴ ┴
doc └───┘ └───┘
240 (s.sum_hom _).symm
id ┴└──────┘ └──┘
src └──────┘ └──┘
typ ┴└──────┘ └──┘
241
242 lemma monic_monomial_eq (m) : monomial m (1:α) = (m.prod $ λn e, X n ^ e : mv_polynomial σ α) :=
id └──────┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴
src └──────┘ ┴ └───┘ ┴ ┴ └───────────┘
typ └──────┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴
doc └──────┘ └───┘ ┴ └───────────┘
243 by simp [monomial_eq]
id └─────────┘
src └────┘└─────────┘└─
typ └────┘└─────────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────────────
244
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
245 @[simp] lemma coeff_monomial (m n) (a) :
doc └──┘
246 coeff m (monomial n a : mv_polynomial σ α) = if n = m then a else 0 :=
id └───┘ ┴ └──────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ └──────┘ └───────────┘ ┴ ┴
typ └───┘ ┴ └──────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ └──────┘ └───────────┘
247 by convert single_apply
id └──────────┘
src └──────┘└──────────┘└
typ └──────┘└──────────┘└
doc └──────┘ └
txt └──────┘ └
par └──────┘ └
pid ┴ └
st └─────────────────────
248
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
249 @[simp] lemma coeff_C (m) (a) :
doc └──┘
250 coeff m (C a : mv_polynomial σ α) = if 0 = m then a else 0 :=
id └───┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ └───────────┘ ┴ ┴
typ └───┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ ┴ └───────────┘
251 by convert single_apply
id └──────────┘
src └──────┘└──────────┘└
typ └──────┘└──────────┘└
doc └──────┘ └
txt └──────┘ └
par └──────┘ └
pid ┴ └
st └─────────────────────
252
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
253 lemma coeff_X_pow (i : σ) (m) (k : ℕ) :
id ┴ ┴
src ┴
typ ┴ ┴
254 coeff m (X i ^ k : mv_polynomial σ α) = if single i k = m then 1 else 0 :=
id └───┘ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ └───────────┘ ┴ └────┘ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴
doc └───┘ ┴ └───────────┘ └────┘
255 begin
st └─────
256 have := coeff_monomial m (finsupp.single i k) (1:α),
id └────────────┘ ┴ └────────────┘ ┴ ┴ ┴
src └──────┘└────────────┘┴ ┴ └────────────┘┴ ┴ └┘ └┘ ┴
typ └──────┘└────────────┘┴┴┴ └────────────┘┴┴┴┴└┘ └┘┴┴
doc └──────┘ ┴ ┴ └────────────┘┴ ┴ └┘ └┘ ┴
txt └──────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴
par └──────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴
pid └───┘└─┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴
st ────────────────────────────────────────────────────┘└─
257 rwa [@monomial_eq _ _ (1:α) (finsupp.single i k) _,
id └─────────┘ ┴ └────────────┘ ┴ ┴
src └───┘ └─────────┘└───┘ └┘ └┘ └────────────┘┴ ┴ └────
typ └───┘ └─────────┘└───┘ └┘┴└┘ └────────────┘┴┴┴┴└────
doc └───┘ └───┘ └┘ └┘ └────────────┘┴ ┴ └────
txt └───┘ └───┘ └┘ └┘ ┴ ┴ └────
par └───┘ └───┘ └┘ └┘ ┴ ┴ └────
pid └┘ └───┘ └┘ └┘ ┴ ┴ └────
st ───────────────────────────────────────────────────┘└─
258 C_1, one_mul, finsupp.prod_single_index] at this,
id └─┘ └─────┘ └───────────────────────┘
src ───┘└─┘└┘└─────┘└┘└───────────────────────┘└───────┘
typ ───┘└─┘└┘└─────┘└┘└───────────────────────┘└───────┘
doc ───┘ └┘ └┘ └───────┘
txt ───┘ └┘ └┘ └───────┘
par ───┘ └┘ └┘ └───────┘
pid ───┘ └┘ └┘ ┴└──────┘
st ──────┘└───────┘└─────────────────────────┘┴└──────┘└─
259 exact pow_zero _
id └──────┘
src └────┘└──────┘└─┘
typ └────┘└──────┘└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └┘┴
st ──────────────────┘
260 end
st └─┘
261
262 lemma coeff_X' (i : σ) (m) :
id ┴
typ ┴
263 coeff m (X i : mv_polynomial σ α) = if single i 1 = m then 1 else 0 :=
id └───┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
src └───┘ ┴ └───────────┘ ┴ └────┘ ┴
typ └───┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
doc └───┘ ┴ └───────────┘ └────┘
264 by rw [← coeff_X_pow, pow_one]
id └─────────┘ └─────┘
src └────┘└─────────┘└┘└─────┘└─
typ └────┘└─────────┘└┘└─────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid └──┘ └┘ ┴└
st └────────────────┘└───────┘┴└
265
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
266 @[simp] lemma coeff_X (i : σ) :
id ┴
typ ┴
doc └──┘
267 coeff (single i 1) (X i : mv_polynomial σ α) = 1 :=
id └───┘ └────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴
src └───┘ └────┘ ┴ └───────────┘ ┴
typ └───┘ └────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴
doc └───┘ └────┘ ┴ └───────────┘
268 by rw [coeff_X', if_pos rfl]
id └──────┘ └────┘ └─┘
src └──┘└──────┘└┘└────┘┴└─┘└─
typ └──┘└──────┘└┘└────┘┴└─┘└─
doc └──┘ └┘ ┴ └─
txt └──┘ └┘ ┴ └─
par └──┘ └┘ ┴ └─
pid └┘ └┘ ┴ ┴└
st └───────────┘└──────────┘┴└
269
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
270 @[simp] lemma coeff_C_mul (m) (a : α) (p : mv_polynomial σ α) : coeff m (C a * p) = a * coeff m p :=
id ┴ └───────────┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
src └───────────┘ └───┘ ┴ ┴ ┴ ┴ └───┘
typ ┴ └───────────┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
doc └──┘ └───────────┘ └───┘ ┴ └───┘
271 begin
st └─────
272 rw [mul_def, C, monomial],
id └─────┘ ┴ └──────┘
src └──┘└─────┘└┘┴└┘└──────┘┴
typ └──┘└─────┘└┘┴└┘└──────┘┴
doc └──┘ └┘┴└┘└──────┘┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ────────────┘└─┘└────────┘└──
273 simp only [sum_single_index, zero_mul, single_zero, zero_add, sum_zero],
id └──────────────┘ └──────┘ └─────────┘ └──────┘ └──────┘
src └─────────┘└──────────────┘└┘└──────┘└┘└─────────┘└┘└──────┘└┘└──────┘┴
typ └─────────┘└──────────────┘└┘└──────┘└┘└─────────┘└┘└──────┘└┘└──────┘┴
doc └─────────┘ └┘ └┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ ┴
st ────────────────────────────────────────────────────────────────────────┘└─
274 convert sum_apply,
id └───────┘
src └──────┘└───────┘
typ └──────┘└───────┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ──────────────────┘└─
275 simp only [single_apply, finsupp.sum],
id └──────────┘ └─────────┘
src └─────────┘└──────────┘└┘└─────────┘┴
typ └─────────┘└──────────┘└┘└─────────┘┴
doc └─────────┘ └┘└─────────┘┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st ──────────────────────────────────────┘└─
276 rw finset.sum_eq_single m,
id └──────────────────┘ ┴
src └─┘└──────────────────┘┴
typ └─┘└──────────────────┘┴┴
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ──────────────────────────┘└─
277 { rw if_pos rfl, refl },
id └────┘ └─┘
src └─┘└────┘┴└─┘ └───┘
typ └─┘└────┘┴└─┘ └───┘
doc └─┘ ┴ └───┘
txt └─┘ ┴ └───┘
par └─┘ ┴ └───┘
pid ┴ ┴ ┴
st ───┘└───────────┘└─────┘└┘└
278 { intros m' hm' H, apply if_neg, exact H },
id └────┘ ┴
src └─────────────┘ └────┘└────┘ └────┘ ┴
typ └─────────────┘ └────┘└────┘ └────┘┴┴
doc └─────────────┘ └────┘ └────┘ ┴
txt └─────────────┘ └────┘ └────┘ ┴
par └─────────────┘ └────┘ └────┘ ┴
pid └───────┘ ┴ ┴ ┴
st ───┘└─────────────┘└────────────┘└────────┘└┘└
279 { intros hm, rw if_pos rfl, rw not_mem_support_iff at hm, simp [hm] }
id └────┘ └─┘ └─────────────────┘ └┘
src └───────┘ └─┘└────┘┴└─┘ └─┘└─────────────────┘└────┘ └────┘ └┘
typ └───────┘ └─┘└────┘┴└─┘ └─┘└─────────────────┘└────┘ └────┘└┘└┘
doc └───────┘ └─┘ ┴ └─┘ └────┘ └────┘ └┘
txt └───────┘ └─┘ ┴ └─┘ └────┘ └────┘ └┘
par └───────┘ └─┘ ┴ └─┘ └────┘ └────┘ └┘
pid └─┘ ┴ ┴ ┴ └────┘ ┴┴ ┴┴
st ────────────┘└─────────────┘└────────────────────────────┘└──────────┘└─
280 end
st ──┘
281
282 lemma coeff_mul (p q : mv_polynomial σ α) (n : σ →₀ ℕ) :
id └───────────┘ ┴ ┴ ┴ └┘ ┴
src └───────────┘ └┘ ┴
typ └───────────┘ ┴ ┴ ┴ └┘ ┴
doc └───────────┘ └┘
283 coeff n (p * q) = finset.sum (antidiagonal n).support (λ x, coeff x.1 p * coeff x.2 q) :=
id └───┘ ┴ ┴ ┴ ┴ ┴ └────────┘ └──────────┘ ┴ └─────┘ ┴ └───┘ ┴┴ ┴ ┴ └───┘ ┴┴ ┴
src └───┘ ┴ ┴ └────────┘ └──────────┘ └─────┘ └───┘ ┴ ┴ └───┘ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ └────────┘ └──────────┘ ┴ └─────┘ ┴ └───┘ ┴┴ ┴ ┴ └───┘ ┴┴ ┴
doc └───┘ └───┘ └───┘
284 begin
st └─────
285 rw mul_def,
id └─────┘
src └─┘└─────┘
typ └─┘└─────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────┘└─
286 have := @finset.sum_sigma (σ →₀ ℕ) α _ _ p.support (λ _, q.support)
id └──────────────┘ ┴ └┘ ┴ └───────┘ └───────┘
src └──────┘ └──────────────┘┴ ┴└┘┴ └┘ └───┘└───────┘┴ └──┘└───────┘└─
typ └──────┘ └──────────────┘┴ ┴┴└┘┴ └┘┴└───┘└───────┘┴ └──┘└───────┘└─
doc └──────┘ ┴ ┴└┘┴ └┘ └───┘ ┴ └──┘ └─
txt └──────┘ ┴ ┴ ┴ └┘ └───┘ ┴ └──┘ └─
par └──────┘ ┴ ┴ ┴ └┘ └───┘ ┴ └──┘ └─
pid └───┘└─┘ ┴ ┴ ┴ └┘ └───┘ ┴ └──┘ └─
st ──────────────────────────────────────────────────────────────────────
287 (λ x, if (x.1 + x.2 = n) then coeff x.1 p * coeff x.2 q else 0),
id ┴ ┴ ┴ ┴ ┴ └───┘ ┴
src ───┘ └──┘ ┴ └─┘┴┴ └─┘┴┴ └─────┘ ┴ └─┘ ┴┴┴└───┘┴ └─┘ └──────┘
typ ───┘ └──┘ ┴ └─┘┴┴ └─┘┴┴┴└─────┘ ┴ └─┘┴┴┴┴└───┘┴ └─┘┴└──────┘
doc ───┘ └──┘ ┴ └─┘ ┴ └─┘ ┴ └─────┘ ┴ └─┘ ┴ ┴└───┘┴ └─┘ └──────┘
txt ───┘ └──┘ ┴ └─┘ ┴ └─┘ ┴ └─────┘ ┴ └─┘ ┴ ┴ ┴ └─┘ └──────┘
par ───┘ └──┘ ┴ └─┘ ┴ └─┘ ┴ └─────┘ ┴ └─┘ ┴ ┴ ┴ └─┘ └──────┘
pid ───┘ └──┘ ┴ └─┘ ┴ └─┘ ┴ └─────┘ ┴ └─┘ ┴ ┴ ┴ └─┘ └──────┘
st ──────────────────────────────────────────────────────────────────┘└─
288 convert this.symm using 1; clear this,
id └───────┘
src └──────┘└───────┘└──────┘ └────────┘
typ └──────┘└───────┘└──────┘ └────────┘
doc └──────┘ └──────┘ └────────┘
txt └──────┘ └──────┘ └────────┘
par └──────┘ └──────┘ └────────┘
pid ┴ └─────┘┴ └───┘
st ──────────────────────────────────────┘└─
289 { rw [coeff],
id └───┘
src └──┘└───┘┴
typ └──┘└───┘┴
doc └──┘└───┘┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ───┘└───────┘└──
290 repeat {rw sum_apply, apply finset.sum_congr rfl, intros, dsimp only},
id └───────┘ └──────────────┘ └─┘
src └──────┘└─┘└───────┘└┘└────┘└──────────────┘┴└─┘└┘└────┘└┘└────────┘┴
typ └──────┘└─┘└───────┘└┘└────┘└──────────────┘┴└─┘└┘└────┘└┘└────────┘┴
doc └──────┘└─┘ └┘└────┘ ┴ └┘└────┘└┘└────────┘┴
txt └──────┘└─┘ └┘└────┘ ┴ └┘└────┘└┘└────────┘┴
par └──────┘└─┘ └┘└────┘ ┴ └┘└────┘└┘└────────┘┴
pid └───┘ └──────┘ ┴ └───────────────────┘
st ───────────────────────┘└──────────────────────────┘└──────┘└──────────┘└┘└
291 convert single_apply },
id └──────────┘
src └──────┘└──────────┘┴
typ └──────┘└──────────┘┴
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid ┴ ┴
st ────────────────────────┘└┘└
292 { have : (antidiagonal n).support.filter (λ x, x.1 ∈ p.support ∧ x.2 ∈ q.support) ⊆
id ┴ └───────┘ └───────┘ ┴
src └─────┘ ┴ └───────────────┘ └──┘ └─┘┴┴└───────┘┴ ┴ └─┘ ┴└───────┘└┘┴└
typ └─────┘ ┴ └───────────────┘ └──┘ └─┘┴┴└───────┘┴ ┴ └─┘ ┴└───────┘└┘┴└
doc └─────┘ ┴ └───────────────┘ └──┘ └─┘ ┴ ┴ ┴ └─┘ ┴ └┘ └
txt └─────┘ ┴ └───────────────┘ └──┘ └─┘ ┴ ┴ ┴ └─┘ ┴ └┘ └
par └─────┘ ┴ └───────────────┘ └──┘ └─┘ ┴ ┴ ┴ └─┘ ┴ └┘ └
pid └───┘└┘ ┴ └───────────────┘ └──┘ └─┘ ┴ ┴ ┴ └─┘ ┴ └┘ └
st ──────────────────────────────────────────────────────────────────────────────────────
293 (antidiagonal n).support := finset.filter_subset _,
id └──────────┘ ┴ └──────────────────┘
src ──────────┘ └──────────┘┴ └───────────┘└──────────────────┘└┘
typ ──────────┘ └──────────┘┴┴└───────────┘└──────────────────┘└┘
doc ──────────┘ ┴ └───────────┘ └┘
txt ──────────┘ ┴ └───────────┘ └┘
par ──────────┘ ┴ └───────────┘ └┘
pid ──────────┘ ┴ └──────┘└───┘ └┘
st ────────────────────────────────────────────────────────────┘└─
294 rw [← finset.sum_sdiff this, finset.sum_eq_zero, zero_add], swap,
id └──────────────┘ └──┘ └────────────────┘ └──────┘
src └────┘└──────────────┘┴ └┘└────────────────┘└┘└──────┘┴ └──┘
typ └────┘└──────────────┘┴└──┘└┘└────────────────┘└┘└──────┘┴ └──┘
doc └────┘ ┴ └┘ └┘ ┴ └──┘
txt └────┘ ┴ └┘ └┘ ┴ └──┘
par └────┘ ┴ └┘ └┘ ┴ └──┘
pid └──┘ ┴ └┘ └┘ ┴
st ──────────────────────────────┘└──────────────────┘└────────┘└─────┘└─
295 { intros x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ─────┘└─────────┘└─
296 rw [finset.mem_sdiff, not_iff_not_of_iff (finset.mem_filter),
id └──────────────┘ └────────────────┘ └───────────────┘
src └──┘└──────────────┘└┘└────────────────┘┴ └───────────────┘└──
typ └──┘└──────────────┘└┘└────────────────┘┴ └───────────────┘└──
doc └──┘ └┘ ┴ └──
txt └──┘ └┘ ┴ └──
par └──┘ └┘ ┴ └──
pid └┘ └┘ ┴ └──
st ─────────────────────────┘└──────────────────────────────────────┘└─
297 not_and, not_and, not_mem_support_iff] at hx,
id └─────┘ └─────┘ └─────────────────┘
src ─────────┘└─────┘└┘└─────┘└┘└─────────────────┘└─────┘
typ ─────────┘└─────┘└┘└─────┘└┘└─────────────────┘└─────┘
doc ─────────┘ └┘ └┘ └─────┘
txt ─────────┘ └┘ └┘ └─────┘
par ─────────┘ └┘ └┘ └─────┘
pid ─────────┘ └┘ └┘ ┴└────┘
st ────────────────┘└───────┘└───────────────────┘┴└────┘└─
298 by_cases H : x.1 ∈ p.support,
id ┴ └───────┘
src └───────┘ └─┘ └─┘ ┴└───────┘
typ └───────┘ └─┘┴└─┘ ┴└───────┘
doc └───────┘ └─┘ └─┘ ┴
txt └───────┘ └─┘ └─┘ ┴
par └───────┘ └─┘ └─┘ ┴
pid ┴ └─┘ └─┘ ┴
st ─────────────────────────────────┘└─
299 { rw [coeff, coeff, hx.2 hx.1 H, mul_zero] },
id └───┘ └───┘ └┘ ┴ └──────┘
src └──┘└───┘└┘└───┘└┘ └─┘ └─┘ └┘└──────┘└┘
typ └──┘└───┘└┘└───┘└┘ └─┘└┘└─┘┴└┘└──────┘└┘
doc └──┘└───┘└┘└───┘└┘ └─┘ └─┘ └┘ └┘
txt └──┘ └┘ └┘ └─┘ └─┘ └┘ └┘
par └──┘ └┘ └┘ └─┘ └─┘ └┘ └┘
pid └┘ └┘ └┘ └─┘ └─┘ └┘ ┴┴
st ───────┘└───────┘└─────┘└───────────┘└────────┘┴┴└┘└
300 { rw not_mem_support_iff at H, rw [coeff, H, zero_mul] } },
id └─────────────────┘ └───┘ ┴ └──────┘
src └─┘└─────────────────┘└───┘ └──┘└───┘└┘ └┘└──────┘└┘
typ └─┘└─────────────────┘└───┘ └──┘└───┘└┘┴└┘└──────┘└┘
doc └─┘ └───┘ └──┘└───┘└┘ └┘ └┘
txt └─┘ └───┘ └──┘ └┘ └┘ └┘
par └─┘ └───┘ └──┘ └┘ └┘ └┘
pid ┴ └───┘ └┘ └┘ └┘ ┴┴
st ──────────────────────────────────┘└─────────┘└─┘└────────┘┴┴└──┘└
301 symmetry,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
st ───────────┘└─
302 rw [← finset.sum_sdiff (finset.filter_subset _), finset.sum_eq_zero, zero_add], swap,
id └──────────────┘ └──────────────────┘ └────────────────┘ └──────┘
src └────┘└──────────────┘┴ └──────────────────┘└───┘└────────────────┘└┘└──────┘┴ └──┘
typ └────┘└──────────────┘┴ └──────────────────┘└───┘└────────────────┘└┘└──────┘┴ └──┘
doc └────┘ ┴ └───┘ └┘ ┴ └──┘
txt └────┘ ┴ └───┘ └┘ ┴ └──┘
par └────┘ ┴ └───┘ └┘ ┴ └──┘
pid └──┘ ┴ └───┘ └┘ ┴
st ──────────────────────────────────────────────────┘└──────────────────┘└────────┘└─────┘└─
303 { intros x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ─────┘└─────────┘└─
304 rw [finset.mem_sdiff, not_iff_not_of_iff (finset.mem_filter), not_and] at hx,
id └──────────────┘ └────────────────┘ └───────────────┘ └─────┘
src └──┘└──────────────┘└┘└────────────────┘┴ └───────────────┘└─┘└─────┘└─────┘
typ └──┘└──────────────┘└┘└────────────────┘┴ └───────────────┘└─┘└─────┘└─────┘
doc └──┘ └┘ ┴ └─┘ └─────┘
txt └──┘ └┘ ┴ └─┘ └─────┘
par └──┘ └┘ ┴ └─┘ └─────┘
pid └┘ └┘ ┴ └─┘ ┴└────┘
st ─────────────────────────┘└──────────────────────────────────────┘└───────┘┴└────┘└─
305 rw if_neg,
id └────┘
src └─┘└────┘
typ └─┘└────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────────┘└─
306 exact hx.2 hx.1 },
id └┘
src └────┘ └─┘ └─┘
typ └────┘ └─┘└┘└─┘
doc └────┘ └─┘ └─┘
txt └────┘ └─┘ └─┘
par └────┘ └─┘ └─┘
pid ┴ └─┘ └─┘
st ─────────────────────┘└┘└
307 { apply finset.sum_bij, swap 5,
id └────────────┘
src └────┘└────────────┘ └────┘
typ └────┘└────────────┘ └────┘
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid ┴ ┴┴
st ─────┘└──────────────────┘└──────┘└─
308 { intros x hx, exact (x.1, x.2) },
id ┴
src └─────────┘ └────┘ └──┘ └──┘
typ └─────────┘ └────┘ └──┘┴└──┘
doc └─────────┘ └────┘ └──┘ └──┘
txt └─────────┘ └────┘ └──┘ └──┘
par └─────────┘ └────┘ └──┘ └──┘
pid └───┘ ┴ └──┘ └─┘┴
st ───────┘└─────────┘└─────────────────┘└┘└
309 { intros x hx, rw [finset.mem_filter, finset.mem_sigma] at hx,
id └───────────────┘ └──────────────┘
src └─────────┘ └──┘└───────────────┘└┘└──────────────┘└─────┘
typ └─────────┘ └──┘└───────────────┘└┘└──────────────┘└─────┘
doc └─────────┘ └──┘ └┘ └─────┘
txt └─────────┘ └──┘ └┘ └─────┘
par └─────────┘ └──┘ └┘ └─────┘
pid └───┘ └┘ └┘ ┴└────┘
st ───────┘└─────────┘└─────────────────────┘└────────────────┘┴└────┘└─
310 simpa [finset.mem_filter, mem_antidiagonal_support] using hx.symm },
id └───────────────┘ └──────────────────────┘ └─────┘
src └─────┘└───────────────┘└┘└──────────────────────┘└──────┘└─────┘┴
typ └─────┘└───────────────┘└┘└──────────────────────┘└──────┘└─────┘┴
doc └─────┘ └┘ └──────┘ ┴
txt └─────┘ └┘ └──────┘ ┴
par └─────┘ └┘ └──────┘ ┴
pid ┴┴ └┘ ┴┴└────┘ ┴
st ─────────────────────────────────────────────────────────────────────────┘└┘└
311 { intros x hx, rw finset.mem_filter at hx, rw if_pos hx.2 },
id └───────────────┘ └────┘ └┘
src └─────────┘ └─┘└───────────────┘└────┘ └─┘└────┘┴ └─┘
typ └─────────┘ └─┘└───────────────┘└────┘ └─┘└────┘┴└┘└─┘
doc └─────────┘ └─┘ └────┘ └─┘ ┴ └─┘
txt └─────────┘ └─┘ └────┘ └─┘ ┴ └─┘
par └─────────┘ └─┘ └────┘ └─┘ ┴ └─┘
pid └───┘ ┴ └────┘ ┴ ┴ └─┘
st ───────┘└─────────┘└──────────────────────────┘└───────────────┘└┘└
312 { rintros ⟨i,j⟩ ⟨k,l⟩ hij hkl, simpa using and.intro },
id └───────┘
src └─────────────────────────┘ └──────────┘└───────┘┴
typ └─────────────────────────┘ └──────────┘└───────┘┴
doc └─────────────────────────┘ └──────────┘ ┴
txt └─────────────────────────┘ └──────────┘ ┴
par └─────────────────────────┘ └──────────┘ ┴
pid └──────────────────┘ ┴└────┘ ┴
st ───────┘└─────────────────────────┘└──────────────────────┘└┘└
313 { rintros ⟨i,j⟩ hij, refine ⟨⟨i,j⟩, _, _⟩, { apply_instance },
id ┴ ┴
src └───────────────┘ └─────┘ ┴ └──────┘ └─────────────┘
typ └───────────────┘ └─────┘ ┴┴┴└──────┘ └─────────────┘
doc └───────────────┘ └─────┘ ┴ └──────┘ └─────────────┘
txt └───────────────┘ └─────┘ ┴ └──────┘ └─────────────┘
par └───────────────┘ └─────┘ ┴ └──────┘ └─────────────┘
pid └────────┘ ┴ ┴ └──────┘ ┴
st ────────────────────────┘└────────────────────┘└──┘└─────────────┘└┘└
314 { rw [finset.mem_filter, mem_antidiagonal_support] at hij,
id └───────────────┘ └──────────────────────┘
src └──┘└───────────────┘└┘└──────────────────────┘└──────┘
typ └──┘└───────────────┘└┘└──────────────────────┘└──────┘
doc └──┘ └┘ └──────┘
txt └──┘ └┘ └──────┘
par └──┘ └┘ └──────┘
pid └┘ └┘ ┴└─────┘
st ─────────┘└───────────────────┘└────────────────────────┘┴└─────┘└─
315 simpa [finset.mem_filter, finset.mem_sigma] using hij.symm },
id └───────────────┘ └──────────────┘ └──────┘
src └─────┘└───────────────┘└┘└──────────────┘└──────┘└──────┘┴
typ └─────┘└───────────────┘└┘└──────────────┘└──────┘└──────┘┴
doc └─────┘ └┘ └──────┘ ┴
txt └─────┘ └┘ └──────┘ ┴
par └─────┘ └┘ └──────┘ ┴
pid ┴┴ └┘ ┴┴└────┘ ┴
st ────────────────────────────────────────────────────────────────────┘└┘└
316 { refl } } },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────────────┘└────┘└
317 all_goals { apply_instance } }
src └──────────┘└─────────────┘└┘
typ └──────────┘└─────────────┘└┘
doc └──────────┘└─────────────┘└┘
txt └──────────┘└─────────────┘└┘
par └──────────┘└─────────────┘└┘
pid └─────────────────┘┴
st ──────────────────────────────┘┴┴└─
318 end
st ──┘
319
320 @[simp] lemma coeff_mul_X (m) (s : σ) (p : mv_polynomial σ α) :
id ┴ └───────────┘ ┴ ┴
src └───────────┘
typ ┴ └───────────┘ ┴ ┴
doc └──┘ └───────────┘
321 coeff (m + single s 1) (p * X s) = coeff m p :=
id └───┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
src └───┘ ┴ └────┘ ┴ ┴ ┴ └───┘
typ └───┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
doc └───┘ └────┘ ┴ └───┘
322 begin
st └─────
323 have : (m, single s 1) ∈ (m + single s 1).antidiagonal.support := mem_antidiagonal_support.2 rfl,
id ┴ ┴ ┴ ┴ └────┘ ┴ └──────────────────────┘ └─┘
src └─────┘┴ └┘ ┴ └──┘┴┴ ┴┴┴└────┘┴ └──────────────────────────┘└──────────────────────┘└─┘└─┘
typ └─────┘┴ └┘ ┴ └──┘┴┴ ┴┴┴┴└────┘┴┴└──────────────────────────┘└──────────────────────┘└─┘└─┘
doc └─────┘ └┘ ┴ └──┘ ┴ ┴ ┴└────┘┴ └──────────────────────────┘ └─┘
txt └─────┘ └┘ ┴ └──┘ ┴ ┴ ┴ ┴ └──────────────────────────┘ └─┘
par └─────┘ └┘ ┴ └──┘ ┴ ┴ ┴ ┴ └──────────────────────────┘ └─┘
pid └───┘└┘ └┘ ┴ └──┘ ┴ ┴ ┴ ┴ └─────────────────────┘└───┘ └─┘
st ─────────────────────────────────────────────────────────────────────────────────────────────────┘└─
324 rw [coeff_mul, ← finset.insert_erase this, finset.sum_insert (finset.not_mem_erase _ _),
id └───────┘ └─────────────────┘ └──┘ └───────────────┘ └──────────────────┘
src └──┘└───────┘└──┘└─────────────────┘┴ └┘└───────────────┘┴ └──────────────────┘└──────
typ └──┘└───────┘└──┘└─────────────────┘┴└──┘└┘└───────────────┘┴ └──────────────────┘└──────
doc └──┘ └──┘ ┴ └┘ ┴ └──────
txt └──┘ └──┘ ┴ └┘ ┴ └──────
par └──┘ └──┘ ┴ └┘ ┴ └──────
pid └┘ └──┘ ┴ └┘ ┴ └──────
st ──────────────┘└──────────────────────────┘└────────────────────────────────────────────┘└─
325 finset.sum_eq_zero, add_zero, coeff_X, mul_one],
id └────────────────┘ └──────┘ └─────┘ └─────┘
src ─────┘└────────────────┘└┘└──────┘└┘└─────┘└┘└─────┘┴
typ ─────┘└────────────────┘└┘└──────┘└┘└─────┘└┘└─────┘┴
doc ─────┘ └┘ └┘ └┘ ┴
txt ─────┘ └┘ └┘ └┘ ┴
par ─────┘ └┘ └┘ └┘ ┴
pid ─────┘ └┘ └┘ └┘ ┴
st ───────────────────────┘└────────┘└───────┘└───────┘└──
326 rintros ⟨i,j⟩ hij,
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
txt └───────────────┘
par └───────────────┘
pid └────────┘
st ──────────────────┘└─
327 rw [finset.mem_erase, mem_antidiagonal_support] at hij,
id └──────────────┘ └──────────────────────┘
src └──┘└──────────────┘└┘└──────────────────────┘└──────┘
typ └──┘└──────────────┘└┘└──────────────────────┘└──────┘
doc └──┘ └┘ └──────┘
txt └──┘ └┘ └──────┘
par └──┘ └┘ └──────┘
pid └┘ └┘ ┴└─────┘
st ─────────────────────┘└────────────────────────┘┴└─────┘└─
328 by_cases H : single s 1 = j,
id └────┘ ┴ ┴ ┴
src └───────┘ └─┘└────┘┴ └─┘┴┴
typ └───────┘ └─┘└────┘┴┴└─┘┴┴┴
doc └───────┘ └─┘└────┘┴ └─┘ ┴
txt └───────┘ └─┘ ┴ └─┘ ┴
par └───────┘ └─┘ ┴ └─┘ ┴
pid ┴ └─┘ ┴ └─┘ ┴
st ────────────────────────────┘└─
329 { subst j, simpa using hij },
id ┴ └─┘
src └────┘ └──────────┘ ┴
typ └────┘┴ └──────────┘└─┘┴
doc └────┘ └──────────┘ ┴
txt └────┘ └──────────┘ ┴
par └────┘ └──────────┘ ┴
pid ┴ ┴└────┘ ┴
st ───┘└─────┘└────────────────┘└┘└
330 { rw [coeff_X', if_neg H, mul_zero] },
id └──────┘ └────┘ ┴ └──────┘
src └──┘└──────┘└┘└────┘┴ └┘└──────┘└┘
typ └──┘└──────┘└┘└────┘┴┴└┘└──────┘└┘
doc └──┘ └┘ ┴ └┘ └┘
txt └──┘ └┘ ┴ └┘ └┘
par └──┘ └┘ ┴ └┘ └┘
pid └┘ └┘ ┴ └┘ ┴┴
st ───────────────┘└────────┘└────────┘┴┴└──
331 end
st ──┘
332
333 lemma coeff_mul_X' (m) (s : σ) (p : mv_polynomial σ α) :
id ┴ └───────────┘ ┴ ┴
src └───────────┘
typ ┴ └───────────┘ ┴ ┴
doc └───────────┘
334 coeff m (p * X s) = if s ∈ m.support then coeff (m - single s 1) p else 0 :=
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──────┘ └───┘ ┴ ┴ └────┘ ┴ ┴
src └───┘ ┴ ┴ ┴ ┴ └──────┘ └───┘ ┴ └────┘
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──────┘ └───┘ ┴ ┴ └────┘ ┴ ┴
doc └───┘ ┴ └───┘ └────┘
335 begin
st └─────
336 split_ifs with h h,
src └────────────────┘
typ └────────────────┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid ┴└──────┘
st ───────────────────┘└─
337 { conv_rhs {rw ← coeff_mul_X _ s},
id └─────────┘ ┴
src └────────┘└───┘└─────────┘└─┘ ┴
typ └────────┘└───┘└─────────┘└─┘┴┴
txt └────────┘└───┘ └─┘ ┴
par └────────┘└───┘ └─┘ ┴
pid ┴└────┘ └─┘ ┴
st ───┘└────────┘└──────────────────┘└┘└
338 congr' 1, ext t,
src └──────┘ └───┘
typ └──────┘ └───┘
doc └──────┘ └───┘
txt └──────┘ └───┘
par └──────┘ └───┘
pid ┴┴ └┘
st ───────────┘└─────┘└─
339 by_cases hj : s = t,
id ┴ ┴ ┴
src └───────┘ └─┘ ┴┴┴
typ └───────┘ └─┘┴┴┴┴┴
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ──────────────────────┘└─
340 { subst t, simp only [nat_sub_apply, add_apply, single_eq_same],
id ┴ └───────────┘ └───────┘ └────────────┘
src └────┘ └─────────┘└───────────┘└┘└───────┘└┘└────────────┘┴
typ └────┘┴ └─────────┘└───────────┘└┘└───────┘└┘└────────────┘┴
doc └────┘ └─────────┘ └┘ └┘ ┴
txt └────┘ └─────────┘ └┘ └┘ ┴
par └────┘ └─────────┘ └┘ └┘ ┴
pid ┴ ┴└──┘└┘ └┘ └┘ ┴
st ─────┘└─────┘└────────────────────────────────────────────────────┘└─
341 refine (nat.sub_add_cancel $ nat.pos_of_ne_zero _).symm, rwa mem_support_iff at h },
id └────────────────┘ └────────────────┘ └─────────────┘
src └─────┘ └────────────────┘┴ ┴└────────────────┘└──────┘ └──┘└─────────────┘└────┘
typ └─────┘ └────────────────┘┴ ┴└────────────────┘└──────┘ └──┘└─────────────┘└────┘
doc └─────┘ ┴ ┴ └──────┘ └──┘ └────┘
txt └─────┘ ┴ ┴ └──────┘ └──┘ └────┘
par └─────┘ ┴ ┴ └──────┘ └──┘ └────┘
pid ┴ ┴ ┴ └─────┘┴ ┴ └───┘┴
st ────────────────────────────────────────────────────────────┘└─────────────────────────┘└┘└
342 { simp [single_eq_of_ne hj] } },
id └─────────────┘ └┘
src └────┘└─────────────┘┴ └┘
typ └────┘└─────────────┘┴└┘└┘
doc └────┘ ┴ └┘
txt └────┘ ┴ └┘
par └────┘ ┴ └┘
pid ┴┴ ┴ ┴┴
st ───────────────────────────────┘└──┘└
343 { delta coeff, rw ← not_mem_support_iff, intro hm, apply h,
id └─────────────────┘
src └─────────┘ └───┘└─────────────────┘ └──────┘ └────┘
typ └─────────┘ └───┘└─────────────────┘ └──────┘ └────┘
doc └─────────┘ └───┘ └──────┘ └────┘
txt └─────────┘ └───┘ └──────┘ └────┘
par └─────────┘ └───┘ └──────┘ └────┘
pid └────┘ └─┘ └─┘ ┴
st ──────────────┘└────────────────────────┘└────────┘└───────┘└─
344 have H := support_mul _ _ hm, simp only [finset.mem_bind] at H,
id └─────────┘ └┘ └─────────────┘
src └────────┘└─────────┘└───┘ └─────────┘└─────────────┘└────┘
typ └────────┘└─────────┘└───┘└┘ └─────────┘└─────────────┘└────┘
doc └────────┘ └───┘ └─────────┘ └────┘
txt └────────┘ └───┘ └─────────┘ └────┘
par └────────┘ └───┘ └─────────┘ └────┘
pid └────┘┴└─┘ └───┘ ┴└──┘└┘ ┴┴└──┘
st ───────────────────────────────┘└────────────────────────────────┘└─
345 rcases H with ⟨j, hj, i', hi', H⟩,
id ┴
src └─────┘ └───────────────────────┘
typ └─────┘┴└───────────────────────┘
doc └─────┘ └───────────────────────┘
txt └─────┘ └───────────────────────┘
par └─────┘ └───────────────────────┘
pid ┴ └───────────────────────┘
st ────────────────────────────────────┘└─
346 delta X monomial at hi', rw mem_support_single at hi', cases hi', subst i',
id └────────────────┘ └─┘ └┘
src └─────────────────────┘ └─┘└────────────────┘└─────┘ └────┘ └────┘
typ └─────────────────────┘ └─┘└────────────────┘└─────┘ └────┘└─┘ └────┘└┘
doc └─────────────────────┘ └─┘ └─────┘ └────┘ └────┘
txt └─────────────────────┘ └─┘ └─────┘ └────┘ └────┘
par └─────────────────────┘ └─┘ └─────┘ └────┘ └────┘
pid └─────────┘└─────┘ ┴ └─────┘ ┴ ┴
st ──────────────────────────┘└────────────────────────────┘└─────────┘└────────┘└─
347 erw finset.mem_singleton at H, subst m,
id └──────────────────┘ ┴
src └──┘└──────────────────┘└───┘ └────┘
typ └──┘└──────────────────┘└───┘ └────┘┴
doc └──┘ └───┘ └────┘
txt └──┘ └───┘ └────┘
par └──┘ └───┘ └────┘
pid ┴ └───┘ ┴
st ────────────────────────────────┘└───────┘└─
348 rw [mem_support_iff, add_apply, single_apply, if_pos rfl],
id └─────────────┘ └───────┘ └──────────┘ └────┘ └─┘
src └──┘└─────────────┘└┘└───────┘└┘└──────────┘└┘└────┘┴└─┘┴
typ └──┘└─────────────┘└┘└───────┘└┘└──────────┘└┘└────┘┴└─┘┴
doc └──┘ └┘ └┘ └┘ ┴ ┴
txt └──┘ └┘ └┘ └┘ ┴ ┴
par └──┘ └┘ └┘ └┘ ┴ ┴
pid └┘ └┘ └┘ └┘ ┴ ┴
st ──────────────────────┘└─────────┘└────────────┘└──────────┘└──
349 intro H, rw [_root_.add_eq_zero_iff] at H, exact one_ne_zero H.2 }
id └────────────────────┘ └─────────┘ ┴
src └─────┘ └──┘└────────────────────┘└────┘ └────┘└─────────┘┴ └─┘
typ └─────┘ └──┘└────────────────────┘└────┘ └────┘└─────────┘┴┴└─┘
doc └─────┘ └──┘ └────┘ └────┘ ┴ └─┘
txt └─────┘ └──┘ └────┘ └────┘ ┴ └─┘
par └─────┘ └──┘ └────┘ └────┘ ┴ └─┘
pid └┘ └┘ ┴└───┘ ┴ ┴ └─┘
st ──────────┘└──────────────────────────┘┴└───┘└──────────────────────┘└─
350 end
st ──┘
351
352 end coeff
353
354 section eval₂
355 variables [comm_semiring β]
id └───────────┘
src └───────────┘
typ └───────────┘
356 variables (f : α → β) (g : σ → β)
id ┴
typ ┴
357
358 /-- Evaluate a polynomial `p` given a valuation `g` of all the variables
359 and a ring hom `f` from the scalar ring to the target -/
360 def eval₂ (p : mv_polynomial σ α) : β :=
id └───────────┘ ┴ ┴ ┴
src └───────────┘
typ └───────────┘ ┴ ┴ ┴
doc └───────────┘
361 p.sum (λs a, f a * s.prod (λn e, g n ^ e))
id ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ └───┘ ┴
typ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └───┘
362
363 @[simp] lemma eval₂_zero : (0 : mv_polynomial σ α).eval₂ f g = 0 :=
id └───────────┘ ┴ ┴ └───┘ ┴ ┴ ┴
src └───────────┘ └───┘ ┴
typ └───────────┘ ┴ ┴ └───┘ ┴ ┴ ┴
doc └──┘ └───────────┘ └───┘
364 finsupp.sum_zero_index
id └────────────────────┘
src └────────────────────┘
typ └────────────────────┘
365
366 section
367 variables [is_semiring_hom f]
id └─────────────┘
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
368
369 @[simp] lemma eval₂_add : (p + q).eval₂ f g = p.eval₂ f g + q.eval₂ f g :=
id ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴└────┘ ┴ ┴
src ┴ └───┘ ┴ └────┘ ┴ └────┘
typ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴└────┘ ┴ ┴
doc └──┘ └───┘ └────┘ └────┘
370 finsupp.sum_add_index
id └───────────────────┘
src └───────────────────┘
typ └───────────────────┘
371 (by simp [is_semiring_hom.map_zero f])
id └──────────────────────┘ ┴
src └────┘└──────────────────────┘┴ ┴
typ └────┘└──────────────────────┘┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴┴ ┴ ┴
st └────────────────────────────────┘
372 (by simp [add_mul, is_semiring_hom.map_add f])
id └─────┘ └─────────────────────┘ ┴
src └────┘└─────┘└┘└─────────────────────┘┴ ┴
typ └────┘└─────┘└┘└─────────────────────┘┴┴┴
doc └────┘ └┘ ┴ ┴
txt └────┘ └┘ ┴ ┴
par └────┘ └┘ ┴ ┴
pid ┴┴ └┘ ┴ ┴
st └────────────────────────────────────────┘
373
374 @[simp] lemma eval₂_monomial : (monomial s a).eval₂ f g = f a * s.prod (λn e, g n ^ e) :=
id └──────┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ └───┘ ┴ ┴ └───┘ ┴
typ └──────┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └──────┘ └───┘ └───┘
375 finsupp.sum_single_index (by simp [is_semiring_hom.map_zero f])
id └──────────────────────┘ └──────────────────────┘ ┴
src └──────────────────────┘ └────┘└──────────────────────┘┴ ┴
typ └──────────────────────┘ └────┘└──────────────────────┘┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴┴ ┴ ┴
st └────────────────────────────────┘
376
377 @[simp] lemma eval₂_C (a) : (C a).eval₂ f g = f a :=
id ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
src ┴ └───┘ ┴
typ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴ └───┘
378 by simp [eval₂_monomial, C, prod_zero_index]
id └────────────┘ ┴ └─────────────┘
src └────┘└────────────┘└┘┴└┘└─────────────┘└─
typ └────┘└────────────┘└┘┴└┘└─────────────┘└─
doc └────┘ └┘┴└┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
st └──────────────────────────────────────────
379
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
380 @[simp] lemma eval₂_one : (1 : mv_polynomial σ α).eval₂ f g = 1 :=
id └───────────┘ ┴ ┴ └───┘ ┴ ┴ ┴
src └───────────┘ └───┘ ┴
typ └───────────┘ ┴ ┴ └───┘ ┴ ┴ ┴
doc └──┘ └───────────┘ └───┘
381 (eval₂_C _ _ _).trans (is_semiring_hom.map_one f)
id └─────┘ └───┘ └─────────────────────┘ ┴
src └─────┘ └───┘ └─────────────────────┘
typ └─────┘ └───┘ └─────────────────────┘ ┴
382
383 @[simp] lemma eval₂_X (n) : (X n).eval₂ f g = g n :=
id ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
src ┴ └───┘ ┴
typ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴ └───┘
384 by simp [eval₂_monomial,
id └────────────┘
src └────┘└────────────┘└─
typ └────┘└────────────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ └─
st └──────────────────────
385 is_semiring_hom.map_one f, X, prod_single_index, pow_one]
id └─────────────────────┘ ┴ ┴ └───────────────┘ └─────┘
src ─┘└─────────────────────┘┴ └┘┴└┘└───────────────┘└┘└─────┘└─
typ ─┘└─────────────────────┘┴┴└┘┴└┘└───────────────┘└┘└─────┘└─
doc ─┘ ┴ └┘┴└┘ └┘ └─
txt ─┘ ┴ └┘ └┘ └┘ └─
par ─┘ ┴ └┘ └┘ └┘ └─
pid ─┘ ┴ └┘ └┘ └┘ ┴└
st ────────────────────────────────────────────────────────────
386
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
387 lemma eval₂_mul_monomial :
388 ∀{s a}, (p * monomial s a).eval₂ f g = p.eval₂ f g * f a * s.prod (λn e, g n ^ e) :=
id ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └──────┘ └───┘ ┴ └────┘ ┴ ┴ └───┘ ┴
typ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────┘ └───┘ └────┘ └───┘
389 begin
st └─────
390 apply mv_polynomial.induction_on p,
id └────────────────────────┘ ┴
src └────┘└────────────────────────┘┴
typ └────┘└────────────────────────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────────────┘└─
391 { assume a' s a,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └───────────┘
st ───┘└───────────┘└─
392 simp [C_mul_monomial, eval₂_monomial, is_semiring_hom.map_mul f] },
id └────────────┘ └────────────┘ └─────────────────────┘ ┴
src └────┘└────────────┘└┘└────────────┘└┘└─────────────────────┘┴ └┘
typ └────┘└────────────┘└┘└────────────┘└┘└─────────────────────┘┴┴└┘
doc └────┘ └┘ └┘ ┴ └┘
txt └────┘ └┘ └┘ ┴ └┘
par └────┘ └┘ └┘ ┴ └┘
pid ┴┴ └┘ └┘ ┴ ┴┴
st ────────────────────────────────────────────────────────────────────┘└┘└
393 { assume p q ih_p ih_q, simp [add_mul, eval₂_add, ih_p, ih_q] },
id └─────┘ └───────┘
src └──────────────────┘ └────┘└─────┘└┘└───────┘└┘ └┘ └┘
typ └──────────────────┘ └────┘└─────┘└┘└───────┘└┘└──┘└┘└──┘└┘
doc └──────────────────┘ └────┘ └┘ └┘ └┘ └┘
txt └──────────────────┘ └────┘ └┘ └┘ └┘ └┘
par └──────────────────┘ └────┘ └┘ └┘ └┘ └┘
pid └──────────────────┘ ┴┴ └┘ └┘ └┘ ┴┴
st ───┘└──────────────────┘└──────────────────────────────────────┘└┘└
394 { assume p n ih s a,
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
txt └───────────────┘
par └───────────────┘
pid └───────────────┘
st ────────────────────┘└─
395 from calc (p * X n * monomial s a).eval₂ f g = (p * monomial (single n 1 + s) a).eval₂ f g :
id ┴ ┴ ┴
src └───┘ ┴ ┴ ┴┴┴ ┴┴┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘┴┴ └┘ └──────┘ ┴ └──
typ └───┘ ┴ ┴ ┴┴┴ ┴┴┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘┴┴ └┘ └──────┘ ┴ └──
doc └───┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └┘ └──────┘ ┴ └──
txt └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └┘ └──────┘ ┴ └──
par └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └┘ └──────┘ ┴ └──
pid └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └┘ └──────┘ ┴ └──
st ─────────────────────────────────────────────────────────────────────────────────────────────────
396 by simp [monomial_single_add, -add_comm, pow_one, mul_assoc]
id └─────────────────┘ └─────┘ └───────┘
src ───────┘ ┴└────┘└─────────────────┘└───────────┘└─────┘└┘└───────┘└─
typ ───────┘ ┴└────┘└─────────────────┘└───────────┘└─────┘└┘└───────┘└─
doc ───────┘ ┴└────┘ └───────────┘ └┘ └─
txt ───────┘ ┴└────┘ └───────────┘ └┘ └─
par ───────┘ ┴└────┘ └───────────┘ └┘ └─
pid ───────┘ └─────┘ └───────────┘ └┘ └─
st ─────────┘└──────────────────────────────────────────────────────────
397 ... = (p * monomial (single n 1) 1).eval₂ f g * f a * s.prod (λn e, g n ^ e) :
id ┴ └──────┘ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴
src ─────┘└──┘ ┴ ┴ ┴└──────┘┴ └────┘┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴└────┘┴ └───┘ ┴ ┴┴┴ └───
typ ─────┘└──┘ ┴ ┴┴ ┴└──────┘┴ └────┘┴┴└───────────┘ ┴ ┴ ┴┴┴┴┴ ┴└────┘┴ └───┘┴┴ ┴┴┴ └───
doc ─────┘└──┘ ┴ ┴ ┴└──────┘┴ └────┘┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴└────┘┴ └───┘ ┴ ┴ ┴ └───
txt ─────┘└──┘ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───
par ─────┘└──┘ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───
pid ─────────┘ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───
st ─────┘└──────────────────────────────────────────────────────────────────────────────
398 by simp [ih, prod_single_index, prod_add_index, pow_one, pow_add, mul_assoc, mul_left_comm,
id └───────────────┘ └────────────┘ └─────┘ └─────┘ └───────┘ └───────────┘
src ───────┘ ┴└────┘ └┘└───────────────┘└┘└────────────┘└┘└─────┘└┘└─────┘└┘└───────┘└┘└───────────┘└─
typ ───────┘ ┴└────┘└┘└┘└───────────────┘└┘└────────────┘└┘└─────┘└┘└─────┘└┘└───────┘└┘└───────────┘└─
doc ───────┘ ┴└────┘ └┘ └┘ └┘ └┘ └┘ └┘ └─
txt ───────┘ ┴└────┘ └┘ └┘ └┘ └┘ └┘ └┘ └─
par ───────┘ ┴└────┘ └┘ └┘ └┘ └┘ └┘ └┘ └─
pid ───────┘ └─────┘ └┘ └┘ └┘ └┘ └┘ └┘ └─
st ─────────┘└─────────────────────────────────────────────────────────────────────────────────────────
399 is_semiring_hom.map_one f, -add_comm] }
id └─────────────────────┘ ┴
src ─────────┘└─────────────────────┘┴ └───────────┘
typ ─────────┘└─────────────────────┘┴┴└───────────┘
doc ─────────┘ ┴ └───────────┘
txt ─────────┘ ┴ └───────────┘
par ─────────┘ ┴ └───────────┘
pid ─────────┘ ┴ └───────────┘
st ───────────────────────────────────────────────┘└─
400 end
st ──┘
401
402 @[simp] lemma eval₂_mul : ∀{p}, (p * q).eval₂ f g = p.eval₂ f g * q.eval₂ f g :=
id ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴└────┘ ┴ ┴
src ┴ └───┘ ┴ └────┘ ┴ └────┘
typ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴└────┘ ┴ ┴
doc └──┘ └───┘ └────┘ └────┘
403 begin
st └─────
404 apply mv_polynomial.induction_on q,
id └────────────────────────┘ ┴
src └────┘└────────────────────────┘┴
typ └────┘└────────────────────────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────────────┘└─
405 { simp [C, eval₂_monomial, eval₂_mul_monomial, prod_zero_index] },
id ┴ └────────────┘ └────────────────┘ └─────────────┘
src └────┘┴└┘└────────────┘└┘└────────────────┘└┘└─────────────┘└┘
typ └────┘┴└┘└────────────┘└┘└────────────────┘└┘└─────────────┘└┘
doc └────┘┴└┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘ └┘
pid ┴┴ └┘ └┘ └┘ ┴┴
st ───┘└────────────────────────────────────────────────────────────┘└┘└
406 { simp [mul_add, eval₂_add] {contextual := tt} },
id └─────┘ └───────┘ └┘
src └────┘└─────┘└┘└───────┘└┘ └────────────┘└┘└┘
typ └────┘└─────┘└┘└───────┘└┘ └────────────┘└┘└┘
doc └────┘ └┘ └┘ └────────────┘ └┘
txt └────┘ └┘ └┘ └────────────┘ └┘
par └────┘ └┘ └┘ └────────────┘ └┘
pid ┴┴ └┘ ┴┴ └────────────┘ ┴┴
st ───┘└───────────────────────────────────────────┘└┘└
407 { simp [X, eval₂_monomial, eval₂_mul_monomial, (mul_assoc _ _ _).symm] { contextual := tt} }
id ┴ └────────────┘ └────────────────┘ └───────┘ └┘
src └────┘┴└┘└────────────┘└┘└────────────────┘└┘ └───────┘└────────────┘ └─────────────┘└┘└┘
typ └────┘┴└┘└────────────┘└┘└────────────────┘└┘ └───────┘└────────────┘ └─────────────┘└┘└┘
doc └────┘┴└┘ └┘ └┘ └────────────┘ └─────────────┘ └┘
txt └────┘ └┘ └┘ └┘ └────────────┘ └─────────────┘ └┘
par └────┘ └┘ └┘ └┘ └────────────┘ └─────────────┘ └┘
pid ┴┴ └┘ └┘ └┘ └───────────┘┴ └─────────────┘ ┴┴
st ────────────────────────────────────────────────────────────────────────────────────────────┘└─
408 end
st ──┘
409
410 @[simp] lemma eval₂_pow {p:mv_polynomial σ α} : ∀{n:ℕ}, (p ^ n).eval₂ f g = (p.eval₂ f g)^n
id └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴└────┘ ┴ ┴ ┴┴
src └───────────┘ ┴ ┴ └───┘ ┴ └────┘ ┴
typ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴└────┘ ┴ ┴ ┴┴
doc └──┘ └───────────┘ └───┘ └────┘
411 | 0 := eval₂_one _ _
id └───────┘
src └───────┘
typ └───────┘
412 | (n + 1) := by rw [pow_add, pow_one, pow_add, pow_one, eval₂_mul, eval₂_pow]
id ┴ └─────┘ └─────┘ └─────┘ └─────┘ └───────┘
src ┴ └──┘└─────┘└┘└─────┘└┘└─────┘└┘└─────┘└┘└───────┘└┘ └─
typ ┴ └──┘└─────┘└┘└─────┘└┘└─────┘└┘└─────┘└┘└───────┘└┘└───────┘└─
doc └──┘ └┘ └┘ └┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ └┘ └┘ ┴└
st └──────────┘└───────┘└───────┘└───────┘└─────────┘└─────────┘┴└
413
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
414 instance eval₂.is_semiring_hom : is_semiring_hom (eval₂ f g) :=
id └─────────────┘ └───┘ ┴ ┴
src └─────────────┘ └───┘
typ └─────────────┘ └───┘ ┴ ┴
doc └─────────────┘ └───┘
415 { map_zero := eval₂_zero _ _,
id └────────┘
src └────────┘
typ └────────┘
416 map_one := eval₂_one _ _,
id └───────┘
src └───────┘
typ └───────┘
417 map_add := λ p q, eval₂_add _ _,
id ┴ ┴ └───────┘
src └───────┘
typ ┴ ┴ └───────┘
418 map_mul := λ p q, eval₂_mul _ _ }
id ┴ ┴ └───────┘
src └───────┘
typ ┴ ┴ └───────┘
419 end
420
421 lemma eval₂_comp_left {γ} [comm_semiring γ]
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
422 (k : β → γ) [is_semiring_hom k]
id ┴ ┴ └─────────────┘ ┴
src └─────────────┘
typ ┴ ┴ └─────────────┘ ┴
doc └─────────────┘
423 (f : α → β) [is_semiring_hom f] (g : σ → β)
id ┴ ┴ └─────────────┘ ┴ ┴ ┴
src └─────────────┘
typ ┴ ┴ └─────────────┘ ┴ ┴ ┴
doc └─────────────┘
424 (p) : k (eval₂ f g p) = eval₂ (k ∘ f) (k ∘ g) p :=
id ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ └───┘ ┴ ┴
typ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ └───┘
425 by apply mv_polynomial.induction_on p; simp [
id └────────────────────────┘ ┴
src └────┘└────────────────────────┘┴ └──────
typ └────┘└────────────────────────┘┴┴ └──────
doc └────┘ ┴ └──────
txt └────┘ ┴ └──────
par └────┘ ┴ └──────
pid ┴ ┴ ┴└─
st └───────────────────────────────────────────
426 eval₂_add, is_semiring_hom.map_add k,
id └───────┘ └─────────────────────┘ ┴
src ─┘└───────┘└┘└─────────────────────┘┴ └─
typ ─┘└───────┘└┘└─────────────────────┘┴┴└─
doc ─┘ └┘ ┴ └─
txt ─┘ └┘ ┴ └─
par ─┘ └┘ ┴ └─
pid ─┘ └┘ ┴ └─
st ────────────────────────────────────────
427 eval₂_mul, is_semiring_hom.map_mul k] {contextual := tt}
id └───────┘ └─────────────────────┘ ┴ └┘
src ─┘└───────┘└┘└─────────────────────┘┴ └┘ └────────────┘└┘└─
typ ─┘└───────┘└┘└─────────────────────┘┴┴└┘ └────────────┘└┘└─
doc ─┘ └┘ ┴ └┘ └────────────┘ └─
txt ─┘ └┘ ┴ └┘ └────────────┘ └─
par ─┘ └┘ ┴ └┘ └────────────┘ └─
pid ─┘ └┘ ┴ ┴┴ └────────────┘ ┴└
st ───────────────────────────────────────────────────────────
428
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
429 @[simp] lemma eval₂_eta (p : mv_polynomial σ α) : eval₂ C X p = p :=
id └───────────┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
src └───────────┘ └───┘ ┴ ┴ ┴
typ └───────────┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
doc └──┘ └───────────┘ └───┘ ┴ ┴
430 by apply mv_polynomial.induction_on p;
id └────────────────────────┘ ┴
src └────┘└────────────────────────┘┴
typ └────┘└────────────────────────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st └────────────────────────────────────
431 simp [eval₂_add, eval₂_mul] {contextual := tt}
id └───────┘ └───────┘ └┘
src └────┘└───────┘└┘└───────┘└┘ └────────────┘└┘└─
typ └────┘└───────┘└┘└───────┘└┘ └────────────┘└┘└─
doc └────┘ └┘ └┘ └────────────┘ └─
txt └────┘ └┘ └┘ └────────────┘ └─
par └────┘ └┘ └┘ └────────────┘ └─
pid ┴┴ └┘ ┴┴ └────────────┘ ┴└
st ──────────────────────────────────────────────────
432
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
433 lemma eval₂_congr (g₁ g₂ : σ → β)
id ┴ ┴
typ ┴ ┴
434 (h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i) :
id ┴ ┴ └┘ ┴ ┴ ┴ ┴└──────┘ └───┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └┘ ┴ ┴ └──────┘ └───┘ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴ ┴ ┴└──────┘ └───┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └┘ └───┘
435 p.eval₂ f g₁ = p.eval₂ f g₂ :=
id ┴└────┘ ┴ └┘ ┴ ┴└────┘ ┴ └┘
src └────┘ ┴ └────┘
typ ┴└────┘ ┴ └┘ ┴ ┴└────┘ ┴ └┘
doc └────┘ └────┘
436 begin
st └─────
437 apply finset.sum_congr rfl,
id └──────────────┘ └─┘
src └────┘└──────────────┘┴└─┘
typ └────┘└──────────────┘┴└─┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────┘└─
438 intros c hc, dsimp, congr' 1,
src └─────────┘ └───┘ └──────┘
typ └─────────┘ └───┘ └──────┘
doc └─────────┘ └───┘ └──────┘
txt └─────────┘ └───┘ └──────┘
par └─────────┘ └───┘ └──────┘
pid └───┘ ┴┴
st ────────────┘└─────┘└────────┘└─
439 apply finset.prod_congr rfl,
id └───────────────┘ └─┘
src └────┘└───────────────┘┴└─┘
typ └────┘└───────────────┘┴└─┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────────────────────┘└─
440 intros i hi, dsimp, congr' 1,
src └─────────┘ └───┘ └──────┘
typ └─────────┘ └───┘ └──────┘
doc └─────────┘ └───┘ └──────┘
txt └─────────┘ └───┘ └──────┘
par └─────────┘ └───┘ └──────┘
pid └───┘ ┴┴
st ────────────┘└─────┘└────────┘└─
441 apply h hi,
id ┴ └┘
src └────┘ ┴
typ └────┘┴┴└┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────┘└─
442 rwa finsupp.mem_support_iff at hc
id └─────────────────────┘
src └──┘└─────────────────────┘└─────┘
typ └──┘└─────────────────────┘└─────┘
doc └──┘ └─────┘
txt └──┘ └─────┘
par └──┘ └─────┘
pid ┴ └────┘┴
st ───────────────────────────────────┘
443 end
st └─┘
444
445 variables [is_semiring_hom f]
id └─────────────┘
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
446
447 @[simp] lemma eval₂_prod (s : finset γ) (p : γ → mv_polynomial σ α) :
id └────┘ ┴ ┴ └───────────┘ ┴ ┴
src └────┘ └───────────┘
typ └────┘ ┴ ┴ └───────────┘ ┴ ┴
doc └──┘ └────┘ └───────────┘
448 eval₂ f g (s.prod p) = s.prod (λ x, eval₂ f g $ p x) :=
id └───┘ ┴ ┴ ┴└───┘ ┴ ┴ ┴└───┘ ┴ └───┘ ┴ ┴ ┴ ┴
src └───┘ └───┘ ┴ └───┘ └───┘
typ └───┘ ┴ ┴ ┴└───┘ ┴ ┴ ┴└───┘ ┴ └───┘ ┴ ┴ ┴ ┴
doc └───┘ └───┘ └───┘ └───┘
449 (s.prod_hom _).symm
id ┴└───────┘ └──┘
src └───────┘ └──┘
typ ┴└───────┘ └──┘
450
451 @[simp] lemma eval₂_sum (s : finset γ) (p : γ → mv_polynomial σ α) :
id └────┘ ┴ ┴ └───────────┘ ┴ ┴
src └────┘ └───────────┘
typ └────┘ ┴ ┴ └───────────┘ ┴ ┴
doc └──┘ └────┘ └───────────┘
452 eval₂ f g (s.sum p) = s.sum (λ x, eval₂ f g $ p x) :=
id └───┘ ┴ ┴ ┴└──┘ ┴ ┴ ┴└──┘ ┴ └───┘ ┴ ┴ ┴ ┴
src └───┘ └──┘ ┴ └──┘ └───┘
typ └───┘ ┴ ┴ ┴└──┘ ┴ ┴ ┴└──┘ ┴ └───┘ ┴ ┴ ┴ ┴
doc └───┘ └───┘
453 (s.sum_hom _).symm
id ┴└──────┘ └──┘
src └──────┘ └──┘
typ ┴└──────┘ └──┘
454
455 attribute [to_additive] eval₂_prod
id └────────┘
src └────────┘
typ └────────┘
doc └─────────┘
456
457 lemma eval₂_assoc (q : γ → mv_polynomial σ α) (p : mv_polynomial γ α) :
id ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴
src └───────────┘ └───────────┘
typ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴
doc └───────────┘ └───────────┘
458 eval₂ f (λ t, eval₂ f g (q t)) p = eval₂ f g (eval₂ C q p) :=
id └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴
src └───┘ └───┘ ┴ └───┘ └───┘ ┴
typ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴
doc └───┘ └───┘ └───┘ └───┘ ┴
459 by { rw eval₂_comp_left (eval₂ f g), congr, funext, simp }
id └─────────────┘ └───┘ ┴ ┴
src └─┘└─────────────┘┴ └───┘┴ ┴ ┴ └───┘ └────┘ └───┘
typ └─┘└─────────────┘┴ └───┘┴┴┴┴┴ └───┘ └────┘ └───┘
doc └─┘ ┴ └───┘┴ ┴ ┴ └────┘ └───┘
txt └─┘ ┴ ┴ ┴ ┴ └───┘ └────┘ └───┘
par └─┘ ┴ ┴ ┴ ┴ └───┘ └────┘ └───┘
pid ┴ ┴ ┴ ┴ ┴ ┴
st └───────────────────────────────┘└─────┘└──────┘└─────┘└┘
460
461 end eval₂
462
463 section eval
464 variables {f : σ → α}
465
466 /-- Evaluate a polynomial `p` given a valuation `f` of all the variables -/
467 def eval (f : σ → α) : mv_polynomial σ α → α := eval₂ id f
id ┴ ┴ └───────────┘ ┴ ┴ ┴ └───┘ └┘ ┴
src └───────────┘ └───┘ └┘
typ ┴ ┴ └───────────┘ ┴ ┴ ┴ └───┘ └┘ ┴
doc └───────────┘ └───┘
468
469 @[simp] lemma eval_zero : (0 : mv_polynomial σ α).eval f = 0 := eval₂_zero _ _
id └───────────┘ ┴ ┴ └──┘ ┴ ┴ └────────┘
src └───────────┘ └──┘ ┴ └────────┘
typ └───────────┘ ┴ ┴ └──┘ ┴ ┴ └────────┘
doc └──┘ └───────────┘ └──┘
470
471 @[simp] lemma eval_add : (p + q).eval f = p.eval f + q.eval f := eval₂_add _ _
id ┴ ┴ ┴ └──┘ ┴ ┴ ┴└───┘ ┴ ┴ ┴└───┘ ┴ └───────┘
src ┴ └──┘ ┴ └───┘ ┴ └───┘ └───────┘
typ ┴ ┴ ┴ └──┘ ┴ ┴ ┴└───┘ ┴ ┴ ┴└───┘ ┴ └───────┘
doc └──┘ └──┘ └───┘ └───┘
472
473 lemma eval_monomial : (monomial s a).eval f = a * s.prod (λn e, f n ^ e) :=
id └──────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ └──┘ ┴ ┴ └───┘ ┴
typ └──────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────┘ └──┘ └───┘
474 eval₂_monomial _ _
id └────────────┘
src └────────────┘
typ └────────────┘
475
476 @[simp] lemma eval_C : ∀ a, (C a).eval f = a := eval₂_C _ _
id ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └─────┘
src ┴ └──┘ ┴ └─────┘
typ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └─────┘
doc └──┘ ┴ └──┘
477
478 @[simp] lemma eval_X : ∀ n, (X n).eval f = f n := eval₂_X _ _
id ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └─────┘
src ┴ └──┘ ┴ └─────┘
typ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └─────┘
doc └──┘ ┴ └──┘
479
480 @[simp] lemma eval_mul : (p * q).eval f = p.eval f * q.eval f := eval₂_mul _ _
id ┴ ┴ ┴ └──┘ ┴ ┴ ┴└───┘ ┴ ┴ ┴└───┘ ┴ └───────┘
src ┴ └──┘ ┴ └───┘ ┴ └───┘ └───────┘
typ ┴ ┴ ┴ └──┘ ┴ ┴ ┴└───┘ ┴ ┴ ┴└───┘ ┴ └───────┘
doc └──┘ └──┘ └───┘ └───┘
481
482 instance eval.is_semiring_hom : is_semiring_hom (eval f) :=
id └─────────────┘ └──┘ ┴
src └─────────────┘ └──┘
typ └─────────────┘ └──┘ ┴
doc └─────────────┘ └──┘
483 eval₂.is_semiring_hom _ _
id └───────────────────┘
src └───────────────────┘
typ └───────────────────┘
484
485 theorem eval_assoc {τ}
486 (f : σ → mv_polynomial τ α) (g : τ → α)
id ┴ └───────────┘ ┴ ┴ ┴ ┴
src └───────────┘
typ ┴ └───────────┘ ┴ ┴ ┴ ┴
doc └───────────┘
487 (p : mv_polynomial σ α) :
id └───────────┘ ┴ ┴
src └───────────┘
typ └───────────┘ ┴ ┴
doc └───────────┘
488 p.eval (eval g ∘ f) = (eval₂ C f p).eval g :=
id ┴└───┘ └──┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └──┘ ┴
src └───┘ └──┘ ┴ ┴ └───┘ ┴ └──┘
typ ┴└───┘ └──┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └──┘ ┴
doc └───┘ └──┘ └───┘ ┴ └──┘
489 begin
st └─────
490 rw eval₂_comp_left (eval g),
id └─────────────┘ └──┘ ┴
src └─┘└─────────────┘┴ └──┘┴ ┴
typ └─┘└─────────────┘┴ └──┘┴┴┴
doc └─┘ ┴ └──┘┴ ┴
txt └─┘ ┴ ┴ ┴
par └─┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ────────────────────────────┘└─
491 unfold eval, congr; funext a; simp
src └─────────┘ └───┘ └──────┘ └───┘
typ └─────────┘ └───┘ └──────┘ └───┘
doc └─────────┘ └──────┘ └───┘
txt └─────────┘ └───┘ └──────┘ └───┘
par └─────────┘ └───┘ └──────┘ └───┘
pid └───┘ └┘ ┴
st ────────────┘└──────────────────────┘
492 end
st └─┘
493
494 end eval
495
496 section map
497 variables [comm_semiring β]
id └───────────┘
src └───────────┘
typ └───────────┘
498 variables (f : α → β)
499
500 /-- `map f p` maps a polynomial `p` across a ring hom `f` -/
501 def map : mv_polynomial σ α → mv_polynomial σ β := eval₂ (C ∘ f) X
id └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
src └───────────┘ └───────────┘ └───┘ ┴ ┴ ┴
typ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
doc └───────────┘ └───────────┘ └───┘ ┴ ┴
502
503 variables [is_semiring_hom f]
id └─────────────┘
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
504
505 @[simp] theorem map_monomial (s : σ →₀ ℕ) (a : α) : map f (monomial s a) = monomial s (f a) :=
id ┴ └┘ ┴ ┴ └─┘ ┴ └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴
src └┘ ┴ └─┘ └──────┘ ┴ └──────┘
typ ┴ └┘ ┴ ┴ └─┘ ┴ └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴
doc └──┘ └┘ └─┘ └──────┘ └──────┘
506 (eval₂_monomial _ _).trans monomial_eq.symm
id └────────────┘ └───┘ └─────────┘└───┘
src └────────────┘ └───┘ └─────────┘└───┘
typ └────────────┘ └───┘ └─────────┘└───┘
507
508 @[simp] theorem map_C : ∀ (a : α), map f (C a : mv_polynomial σ α) = C (f a) := map_monomial _ _
id ┴ └─┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘
src └─┘ ┴ └───────────┘ ┴ ┴ └──────────┘
typ ┴ └─┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘
doc └──┘ └─┘ ┴ └───────────┘ ┴
509
510 @[simp] theorem map_X : ∀ (n : σ), map f (X n : mv_polynomial σ α) = X n := eval₂_X _ _
id ┴ └─┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ └─────┘
src └─┘ ┴ └───────────┘ ┴ ┴ └─────┘
typ ┴ └─┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ └─────┘
doc └──┘ └─┘ ┴ └───────────┘ ┴
511
512 @[simp] theorem map_one : map f (1 : mv_polynomial σ α) = 1 := eval₂_one _ _
id └─┘ ┴ └───────────┘ ┴ ┴ ┴ └───────┘
src └─┘ └───────────┘ ┴ └───────┘
typ └─┘ ┴ └───────────┘ ┴ ┴ ┴ └───────┘
doc └──┘ └─┘ └───────────┘
513
514 @[simp] theorem map_add (p q : mv_polynomial σ α) :
id └───────────┘ ┴ ┴
src └───────────┘
typ └───────────┘ ┴ ┴
doc └──┘ └───────────┘
515 map f (p + q) = map f p + map f q := eval₂_add _ _
id └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └───────┘
src └─┘ ┴ ┴ └─┘ ┴ └─┘ └───────┘
typ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └───────┘
doc └─┘ └─┘ └─┘
516
517 @[simp] theorem map_mul (p q : mv_polynomial σ α) :
id └───────────┘ ┴ ┴
src └───────────┘
typ └───────────┘ ┴ ┴
doc └──┘ └───────────┘
518 map f (p * q) = map f p * map f q := eval₂_mul _ _
id └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └───────┘
src └─┘ ┴ ┴ └─┘ ┴ └─┘ └───────┘
typ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └───────┘
doc └─┘ └─┘ └─┘
519
520 @[simp] lemma map_pow (p : mv_polynomial σ α) (n : ℕ) :
id └───────────┘ ┴ ┴ ┴
src └───────────┘ ┴
typ └───────────┘ ┴ ┴ ┴
doc └──┘ └───────────┘
521 map f (p^n) = (map f p)^n := eval₂_pow _ _
id └─┘ ┴ ┴┴┴ ┴ └─┘ ┴ ┴ ┴┴ └───────┘
src └─┘ ┴ ┴ └─┘ ┴ └───────┘
typ └─┘ ┴ ┴┴┴ ┴ └─┘ ┴ ┴ ┴┴ └───────┘
doc └─┘ └─┘
522
523 instance map.is_semiring_hom :
524 is_semiring_hom (map f : mv_polynomial σ α → mv_polynomial σ β) :=
id └─────────────┘ └─┘ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴
src └─────────────┘ └─┘ └───────────┘ └───────────┘
typ └─────────────┘ └─┘ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴
doc └─────────────┘ └─┘ └───────────┘ └───────────┘
525 eval₂.is_semiring_hom _ _
id └───────────────────┘
src └───────────────────┘
typ └───────────────────┘
526
527 theorem map_id : ∀ (p : mv_polynomial σ α), map id p = p := eval₂_eta
id └───────────┘ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ └───────┘
src └───────────┘ └─┘ └┘ ┴ └───────┘
typ └───────────┘ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ └───────┘
doc └───────────┘ └─┘
528
529 theorem map_map [comm_semiring γ]
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
530 (g : β → γ) [is_semiring_hom g]
id ┴ ┴ └─────────────┘ ┴
src └─────────────┘
typ ┴ ┴ └─────────────┘ ┴
doc └─────────────┘
531 (p : mv_polynomial σ α) :
id └───────────┘ ┴ ┴
src └───────────┘
typ └───────────┘ ┴ ┴
doc └───────────┘
532 map g (map f p) = map (g ∘ f) p :=
id └─┘ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src └─┘ └─┘ ┴ └─┘ ┴
typ └─┘ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
doc └─┘ └─┘ └─┘
533 (eval₂_comp_left (map g) (C ∘ f) X p).trans $
id └─────────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘
src └─────────────┘ └─┘ ┴ ┴ ┴ └───┘
typ └─────────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘
doc └─┘ ┴ ┴
534 by congr; funext a; simp
src └───┘ └──────┘ └────
typ └───┘ └──────┘ └────
doc └──────┘ └────
txt └───┘ └──────┘ └────
par └───┘ └──────┘ └────
pid └┘ └
st └──────────────────────
535
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
536 theorem eval₂_eq_eval_map (g : σ → β) (p : mv_polynomial σ α) :
id ┴ ┴ └───────────┘ ┴ ┴
src └───────────┘
typ ┴ ┴ └───────────┘ ┴ ┴
doc └───────────┘
537 p.eval₂ f g = (map f p).eval g :=
id ┴└────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴
src └────┘ ┴ └─┘ └──┘
typ ┴└────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴
doc └────┘ └─┘ └──┘
538 begin
st └─────
539 unfold map eval,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └───────┘
st ────────────────┘└─
540 rw eval₂_comp_left (eval₂ id g),
id └─────────────┘ └───┘ └┘ ┴
src └─┘└─────────────┘┴ └───┘┴└┘┴ ┴
typ └─┘└─────────────┘┴ └───┘┴└┘┴┴┴
doc └─┘ ┴ └───┘┴ ┴ ┴
txt └─┘ ┴ ┴ ┴ ┴
par └─┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────┘└─
541 congr; funext a; simp
src └───┘ └──────┘ └───┘
typ └───┘ └──────┘ └───┘
doc └──────┘ └───┘
txt └───┘ └──────┘ └───┘
par └───┘ └──────┘ └───┘
pid └┘ ┴
st ───────────────────────┘
542 end
st └─┘
543
544 lemma eval₂_comp_right {γ} [comm_semiring γ]
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
545 (k : β → γ) [is_semiring_hom k]
id ┴ ┴ └─────────────┘ ┴
src └─────────────┘
typ ┴ ┴ └─────────────┘ ┴
doc └─────────────┘
546 (f : α → β) [is_semiring_hom f] (g : σ → β)
id ┴ ┴ └─────────────┘ ┴ ┴ ┴
src └─────────────┘
typ ┴ ┴ └─────────────┘ ┴ ┴ ┴
doc └─────────────┘
547 (p) : k (eval₂ f g p) = eval₂ k (k ∘ g) (map f p) :=
id ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
src └───┘ ┴ └───┘ ┴ └─┘
typ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
doc └───┘ └───┘ └─┘
548 begin
st └─────
549 apply mv_polynomial.induction_on p,
id └────────────────────────┘ ┴
src └────┘└────────────────────────┘┴
typ └────┘└────────────────────────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────────────┘└─
550 { intro r, rw [eval₂_C, map_C, eval₂_C] },
id └─────┘ └───┘ └─────┘
src └─────┘ └──┘└─────┘└┘└───┘└┘└─────┘└┘
typ └─────┘ └──┘└─────┘└┘└───┘└┘└─────┘└┘
doc └─────┘ └──┘ └┘ └┘ └┘
txt └─────┘ └──┘ └┘ └┘ └┘
par └─────┘ └──┘ └┘ └┘ └┘
pid └┘ └┘ └┘ └┘ ┴┴
st ───┘└─────┘└───────────┘└─────┘└───────┘┴┴└┘└
551 { intros p q hp hq, rw [eval₂_add, is_semiring_hom.map_add k, map_add, eval₂_add, hp, hq] },
id └───────┘ └─────────────────────┘ ┴ └─────┘ └───────┘ └┘ └┘
src └──────────────┘ └──┘└───────┘└┘└─────────────────────┘┴ └┘└─────┘└┘└───────┘└┘ └┘ └┘
typ └──────────────┘ └──┘└───────┘└┘└─────────────────────┘┴┴└┘└─────┘└┘└───────┘└┘└┘└┘└┘└┘
doc └──────────────┘ └──┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘
txt └──────────────┘ └──┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘
par └──────────────┘ └──┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘
pid └────────┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ ┴┴
st ───┘└──────────────┘└─────────────┘└─────────────────────────┘└───────┘└─────────┘└──┘└──┘┴┴└┘└
552 { intros p s hp,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └─────┘
st ────────────────┘└─
553 rw [eval₂_mul, is_semiring_hom.map_mul k, map_mul, eval₂_mul, map_X, hp, eval₂_X, eval₂_X] }
id └───────┘ └─────────────────────┘ ┴ └─────┘ └───────┘ └───┘ └┘ └─────┘ └─────┘
src └──┘└───────┘└┘└─────────────────────┘┴ └┘└─────┘└┘└───────┘└┘└───┘└┘ └┘└─────┘└┘└─────┘└┘
typ └──┘└───────┘└┘└─────────────────────┘┴┴└┘└─────┘└┘└───────┘└┘└───┘└┘└┘└┘└─────┘└┘└─────┘└┘
doc └──┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘ └┘
txt └──┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘ └┘
par └──┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘ └┘
pid └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘ ┴┴
st ────────────────┘└─────────────────────────┘└───────┘└─────────┘└─────┘└──┘└───────┘└───────┘┴┴└─
554 end
st ──┘
555
556 lemma map_eval₂ (f : α → β) [is_semiring_hom f] (g : γ → mv_polynomial δ α) (p : mv_polynomial γ α) :
id ┴ ┴ └─────────────┘ ┴ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴
src └─────────────┘ └───────────┘ └───────────┘
typ ┴ ┴ └─────────────┘ ┴ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴
doc └─────────────┘ └───────────┘ └───────────┘
557 map f (eval₂ C g p) = eval₂ C (map f ∘ g) (map f p) :=
id └─┘ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
src └─┘ └───┘ ┴ ┴ └───┘ ┴ └─┘ ┴ └─┘
typ └─┘ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
doc └─┘ └───┘ ┴ └───┘ ┴ └─┘ └─┘
558 begin
st └─────
559 apply mv_polynomial.induction_on p,
id └────────────────────────┘ ┴
src └────┘└────────────────────────┘┴
typ └────┘└────────────────────────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────────────┘└─
560 { intro r, rw [eval₂_C, map_C, map_C, eval₂_C] },
id └─────┘ └───┘ └───┘ └─────┘
src └─────┘ └──┘└─────┘└┘└───┘└┘└───┘└┘└─────┘└┘
typ └─────┘ └──┘└─────┘└┘└───┘└┘└───┘└┘└─────┘└┘
doc └─────┘ └──┘ └┘ └┘ └┘ └┘
txt └─────┘ └──┘ └┘ └┘ └┘ └┘
par └─────┘ └──┘ └┘ └┘ └┘ └┘
pid └┘ └┘ └┘ └┘ └┘ ┴┴
st ───┘└─────┘└───────────┘└─────┘└─────┘└───────┘┴┴└┘└
561 { intros p q hp hq, rw [eval₂_add, map_add, hp, hq, map_add, eval₂_add] },
id └───────┘ └─────┘ └┘ └┘ └─────┘ └───────┘
src └──────────────┘ └──┘└───────┘└┘└─────┘└┘ └┘ └┘└─────┘└┘└───────┘└┘
typ └──────────────┘ └──┘└───────┘└┘└─────┘└┘└┘└┘└┘└┘└─────┘└┘└───────┘└┘
doc └──────────────┘ └──┘ └┘ └┘ └┘ └┘ └┘ └┘
txt └──────────────┘ └──┘ └┘ └┘ └┘ └┘ └┘ └┘
par └──────────────┘ └──┘ └┘ └┘ └┘ └┘ └┘ └┘
pid └────────┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴┴
st ───┘└──────────────┘└─────────────┘└───────┘└──┘└──┘└───────┘└─────────┘┴┴└┘└
562 { intros p s hp,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └─────┘
st ────────────────┘└─
563 rw [eval₂_mul, map_mul, hp, map_mul, map_X, eval₂_mul, eval₂_X, eval₂_X] }
id └───────┘ └─────┘ └┘ └─────┘ └───┘ └───────┘ └─────┘ └─────┘
src └──┘└───────┘└┘└─────┘└┘ └┘└─────┘└┘└───┘└┘└───────┘└┘└─────┘└┘└─────┘└┘
typ └──┘└───────┘└┘└─────┘└┘└┘└┘└─────┘└┘└───┘└┘└───────┘└┘└─────┘└┘└─────┘└┘
doc └──┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
txt └──┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
pid └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴┴
st ────────────────┘└───────┘└──┘└───────┘└─────┘└─────────┘└───────┘└───────┘┴┴└─
564 end
st ──┘
565
566 lemma coeff_map (p : mv_polynomial σ α) : ∀ (m : σ →₀ ℕ), coeff m (p.map f) = f (coeff m p) :=
id └───────────┘ ┴ ┴ ┴ └┘ ┴ └───┘ ┴ ┴└──┘ ┴ ┴ ┴ └───┘ ┴ ┴
src └───────────┘ └┘ ┴ └───┘ └──┘ ┴ └───┘
typ └───────────┘ ┴ ┴ ┴ └┘ ┴ └───┘ ┴ ┴└──┘ ┴ ┴ ┴ └───┘ ┴ ┴
doc └───────────┘ └┘ └───┘ └──┘ └───┘
567 begin
st └─────
568 apply mv_polynomial.induction_on p; clear p,
id └────────────────────────┘ ┴
src └────┘└────────────────────────┘┴ └─────┘
typ └────┘└────────────────────────┘┴┴ └─────┘
doc └────┘ ┴ └─────┘
txt └────┘ ┴ └─────┘
par └────┘ ┴ └─────┘
pid ┴ ┴ └┘
st ────────────────────────────────────────────┘└─
569 { intros r m, rw [map_C], simp only [coeff_C], split_ifs, {refl}, rw is_semiring_hom.map_zero f },
id └───┘ └─────┘ └──────────────────────┘ ┴
src └────────┘ └──┘└───┘┴ └─────────┘└─────┘┴ └───────┘ └──┘ └─┘└──────────────────────┘┴ ┴
typ └────────┘ └──┘└───┘┴ └─────────┘└─────┘┴ └───────┘ └──┘ └─┘└──────────────────────┘┴┴┴
doc └────────┘ └──┘ ┴ └─────────┘ ┴ └───────┘ └──┘ └─┘ ┴ ┴
txt └────────┘ └──┘ ┴ └─────────┘ ┴ └───────┘ └──┘ └─┘ ┴ ┴
par └────────┘ └──┘ ┴ └─────────┘ ┴ └───────┘ └──┘ └─┘ ┴ ┴
pid └──┘ └┘ ┴ ┴└──┘└┘ ┴ ┴ ┴ ┴
st ───┘└────────┘└─────────┘└────────────────────┘└─────────┘└─────┘└┘└─────────────────────────────┘└┘└
570 { intros p q hp hq m, simp only [hp, hq, map_add, coeff_add], rw is_semiring_hom.map_add f },
id └┘ └┘ └─────┘ └───────┘ └─────────────────────┘ ┴
src └────────────────┘ └─────────┘ └┘ └┘└─────┘└┘└───────┘┴ └─┘└─────────────────────┘┴ ┴
typ └────────────────┘ └─────────┘└┘└┘└┘└┘└─────┘└┘└───────┘┴ └─┘└─────────────────────┘┴┴┴
doc └────────────────┘ └─────────┘ └┘ └┘ └┘ ┴ └─┘ ┴ ┴
txt └────────────────┘ └─────────┘ └┘ └┘ └┘ ┴ └─┘ ┴ ┴
par └────────────────┘ └─────────┘ └┘ └┘ └┘ ┴ └─┘ ┴ ┴
pid └──────────┘ ┴└──┘└┘ └┘ └┘ └┘ ┴ ┴ ┴ ┴
st ───┘└────────────────┘└──────────────────────────────────────┘└─────────────────────────────┘└┘└
571 { intros p i hp m, simp only [hp, map_mul, map_X],
id └┘ └─────┘ └───┘
src └─────────────┘ └─────────┘ └┘└─────┘└┘└───┘┴
typ └─────────────┘ └─────────┘└┘└┘└─────┘└┘└───┘┴
doc └─────────────┘ └─────────┘ └┘ └┘ ┴
txt └─────────────┘ └─────────┘ └┘ └┘ ┴
par └─────────────┘ └─────────┘ └┘ └┘ ┴
pid └───────┘ ┴└──┘└┘ └┘ └┘ ┴
st ──────────────────┘└──────────────────────────────┘└─
572 simp only [hp, mem_support_iff, coeff_mul_X'],
id └┘ └─────────────┘ └──────────┘
src └─────────┘ └┘└─────────────┘└┘└──────────┘┴
typ └─────────┘└┘└┘└─────────────┘└┘└──────────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ────────────────────────────────────────────────┘└─
573 split_ifs, {refl},
src └───────┘ └──┘
typ └───────┘ └──┘
doc └───────┘ └──┘
txt └───────┘ └──┘
par └───────┘ └──┘
st ────────────┘└─────┘└┘└
574 rw is_semiring_hom.map_zero f }
id └──────────────────────┘ ┴
src └─┘└──────────────────────┘┴ ┴
typ └─┘└──────────────────────┘┴┴┴
doc └─┘ ┴ ┴
txt └─┘ ┴ ┴
par └─┘ ┴ ┴
pid ┴ ┴ ┴
st ─────────────────────────────────┘└─
575 end
st ──┘
576
577 lemma map_injective (hf : function.injective f) :
id └────────────────┘ ┴
src └────────────────┘
typ └────────────────┘ ┴
578 function.injective (map f : mv_polynomial σ α → mv_polynomial σ β) :=
id └────────────────┘ └─┘ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴
src └────────────────┘ └─┘ └───────────┘ └───────────┘
typ └────────────────┘ └─┘ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴
doc └─┘ └───────────┘ └───────────┘
579 λ p q h, ext _ _ $ λ m, hf $
id ┴ ┴ ┴ └─┘ ┴ └┘
src └─┘
typ ┴ ┴ ┴ └─┘ ┴ └┘
580 begin
st └─────
581 rw ← ext_iff at h,
id └─────┘
src └───┘└─────┘└───┘
typ └───┘└─────┘└───┘
doc └───┘ └───┘
txt └───┘ └───┘
par └───┘ └───┘
pid └─┘ └───┘
st ──────────────────┘└─
582 specialize h m,
id ┴ ┴
src └─────────┘ ┴
typ └─────────┘┴┴┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴ ┴
st ───────────────┘└─
583 rw [coeff_map, coeff_map] at h,
id └───────┘ └───────┘
src └──┘└───────┘└┘└───────┘└────┘
typ └──┘└───────┘└┘└───────┘└────┘
doc └──┘ └┘ └────┘
txt └──┘ └┘ └────┘
par └──┘ └┘ └────┘
pid └┘ └┘ ┴└───┘
st ──────────────┘└─────────┘┴└───┘└─
584 exact h
id ┴
src └────┘ ┴
typ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────┘
585 end
st └─┘
586
587 end map
588
589 section degrees
590
591 section comm_semiring
592
593 /--
594 The maximal degrees of each variable in a multi-variable polynomial, expressed as a multiset.
595
596 (For example, `degrees (x^2 * y + y^3)` would be `{x, x, y, y, y}`.)
597 -/
598 def degrees (p : mv_polynomial σ α) : multiset σ :=
id └───────────┘ ┴ ┴ └──────┘ ┴
src └───────────┘ └──────┘
typ └───────────┘ ┴ ┴ └──────┘ ┴
doc └───────────┘ └──────┘
599 p.support.sup (λs:σ →₀ ℕ, s.to_multiset)
id ┴└──────┘└──┘ ┴ └┘ ┴ ┴└──────────┘
src └──────┘└──┘ └┘ ┴ └──────────┘
typ ┴└──────┘└──┘ ┴ └┘ ┴ ┴└──────────┘
doc └──┘ └┘
600
601 lemma degrees_monomial (s : σ →₀ ℕ) (a : α) : degrees (monomial s a) ≤ s.to_multiset :=
id ┴ └┘ ┴ ┴ └─────┘ └──────┘ ┴ ┴ ┴ ┴└──────────┘
src └┘ ┴ └─────┘ └──────┘ ┴ └──────────┘
typ ┴ └┘ ┴ ┴ └─────┘ └──────┘ ┴ ┴ ┴ ┴└──────────┘
doc └┘ └─────┘ └──────┘
602 finset.sup_le $ assume t h,
id └───────────┘ ┴ ┴
src └───────────┘
typ └───────────┘ ┴ ┴
603 begin
st └─────
604 have := finsupp.support_single_subset h,
id └───────────────────────────┘ ┴
src └──────┘└───────────────────────────┘┴
typ └──────┘└───────────────────────────┘┴┴
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid └───┘└─┘ ┴
st ────────────────────────────────────────┘└─
605 rw [finset.singleton_eq_singleton, finset.mem_singleton] at this,
id └───────────────────────────┘ └──────────────────┘
src └──┘└───────────────────────────┘└┘└──────────────────┘└───────┘
typ └──┘└───────────────────────────┘└┘└──────────────────┘└───────┘
doc └──┘ └┘ └───────┘
txt └──┘ └┘ └───────┘
par └──┘ └┘ └───────┘
pid └┘ └┘ ┴└──────┘
st ──────────────────────────────────┘└────────────────────┘┴└──────┘└─
606 rw this
id └──┘
src └─┘ ┴
typ └─┘└──┘┴
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ─────────┘
607 end
st └─┘
608
609 lemma degrees_monomial_eq (s : σ →₀ ℕ) (a : α) (ha : a ≠ 0) :
id ┴ └┘ ┴ ┴ ┴ ┴
src └┘ ┴ ┴
typ ┴ └┘ ┴ ┴ ┴ ┴
doc └┘
610 degrees (monomial s a) = s.to_multiset :=
id └─────┘ └──────┘ ┴ ┴ ┴ ┴└──────────┘
src └─────┘ └──────┘ ┴ └──────────┘
typ └─────┘ └──────┘ ┴ ┴ ┴ ┴└──────────┘
doc └─────┘ └──────┘
611 le_antisymm (degrees_monomial s a) $ finset.le_sup $
id └─────────┘ └──────────────┘ ┴ ┴ └───────────┘
src └─────────┘ └──────────────┘ └───────────┘
typ └─────────┘ └──────────────┘ ┴ ┴ └───────────┘
612 by rw [monomial, finsupp.support_single_ne_zero ha,
id └──────┘ └────────────────────────────┘ └┘
src └──┘└──────┘└┘└────────────────────────────┘┴ └─
typ └──┘└──────┘└┘└────────────────────────────┘┴└┘└─
doc └──┘└──────┘└┘ ┴ └─
txt └──┘ └┘ ┴ └─
par └──┘ └┘ ┴ └─
pid └┘ └┘ ┴ └─
st └───────────┘└─────────────────────────────────┘└─
613 finset.singleton_eq_singleton, finset.mem_singleton]
id └───────────────────────────┘ └──────────────────┘
src ───┘└───────────────────────────┘└┘└──────────────────┘└─
typ ───┘└───────────────────────────┘└┘└──────────────────┘└─
doc ───┘ └┘ └─
txt ───┘ └┘ └─
par ───┘ └┘ └─
pid ───┘ └┘ ┴└
st ────────────────────────────────┘└────────────────────┘┴└
614
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
615 lemma degrees_C (a : α) : degrees (C a : mv_polynomial σ α) = 0 :=
id ┴ └─────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴
src └─────┘ ┴ └───────────┘ ┴
typ ┴ └─────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴
doc └─────┘ ┴ └───────────┘
616 multiset.le_zero.1 $ degrees_monomial _ _
id └──────────────┘┴ └──────────────┘
src └──────────────┘┴ └──────────────┘
typ └──────────────┘┴ └──────────────┘
617
618 lemma degrees_X (n : σ) : degrees (X n : mv_polynomial σ α) ≤ {n} :=
id ┴ └─────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴┴
src └─────┘ ┴ └───────────┘ ┴ ┴
typ ┴ └─────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴┴
doc └─────┘ ┴ └───────────┘
619 le_trans (degrees_monomial _ _) $ le_of_eq $ to_multiset_single _ _
id └──────┘ └──────────────┘ └──────┘ └────────────────┘
src └──────┘ └──────────────┘ └──────┘ └────────────────┘
typ └──────┘ └──────────────┘ └──────┘ └────────────────┘
620
621 lemma degrees_zero : degrees (0 : mv_polynomial σ α) = 0 :=
id └─────┘ └───────────┘ ┴ ┴ ┴
src └─────┘ └───────────┘ ┴
typ └─────┘ └───────────┘ ┴ ┴ ┴
doc └─────┘ └───────────┘
622 by { rw ← C_0, exact degrees_C 0 }
id └─┘ └───────┘
src └───┘└─┘ └────┘└───────┘└─┘
typ └───┘└─┘ └────┘└───────┘└─┘
doc └───┘ └────┘ └─┘
txt └───┘ └────┘ └─┘
par └───┘ └────┘ └─┘
pid └─┘ ┴ ┴└┘
st └─────────┘└──────────────────┘└┘
623
624 lemma degrees_one : degrees (1 : mv_polynomial σ α) = 0 := degrees_C 1
id └─────┘ └───────────┘ ┴ ┴ ┴ └───────┘
src └─────┘ └───────────┘ ┴ └───────┘
typ └─────┘ └───────────┘ ┴ ┴ ┴ └───────┘
doc └─────┘ └───────────┘
625
626 lemma degrees_add (p q : mv_polynomial σ α) : (p + q).degrees ≤ p.degrees ⊔ q.degrees :=
id └───────────┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴└──────┘ ┴ ┴└──────┘
src └───────────┘ ┴ └─────┘ ┴ └──────┘ ┴ └──────┘
typ └───────────┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴└──────┘ ┴ ┴└──────┘
doc └───────────┘ └─────┘ └──────┘ └──────┘
627 begin
st └─────
628 refine finset.sup_le (assume b hb, _),
id └───────────┘
src └─────┘└───────────┘┴ └───────┘
typ └─────┘└───────────┘┴ └───────┘
doc └─────┘ ┴ └───────┘
txt └─────┘ ┴ └───────┘
par └─────┘ ┴ └───────┘
pid ┴ ┴ └───────┘
st ──────────────────────────────────────┘└─
629 have := finsupp.support_add hb, rw finset.mem_union at this,
id └─────────────────┘ └┘ └──────────────┘
src └──────┘└─────────────────┘┴ └─┘└──────────────┘└──────┘
typ └──────┘└─────────────────┘┴└┘ └─┘└──────────────┘└──────┘
doc └──────┘ ┴ └─┘ └──────┘
txt └──────┘ ┴ └─┘ └──────┘
par └──────┘ ┴ └─┘ └──────┘
pid └───┘└─┘ ┴ ┴ └──────┘
st ───────────────────────────────┘└───────────────────────────┘└┘
630 cases this,
631 { exact le_sup_left_of_le (finset.le_sup this) },
st └┘
632 { exact le_sup_right_of_le (finset.le_sup this) },
st └┘
633 end
st └─┘
634
635 lemma degrees_sum {ι : Type*} (s : finset ι) (f : ι → mv_polynomial σ α) :
id ┴ └┘ ┴ ┴ ┴ ┴
src ┴ └┘
typ ┴ └┘ ┴ ┴ ┴ ┴
doc ┴ └┘
636 (s.sum f).degrees ≤ s.sup (λi, (f i).degrees) :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
637 begin
638 refine s.induction _ _,
639 { simp only [finset.sum_empty, finset.sup_empty, degrees_zero], exact le_refl _ },
st └┘
640 { assume i s his ih,
641 rw [finset.sup_insert, finset.sum_insert his],
642 exact le_trans (degrees_add _ _) (sup_le_sup_left ih _) }
st └─
643 end
st ──┘
644
645 lemma degrees_mul (p q : mv_polynomial σ α) : (p * q).degrees ≤ p.degrees + q.degrees :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
646 begin
647 refine finset.sup_le (assume b hb, _),
648 have := support_mul p q hb,
id ┴ ┴
typ ┴ ┴
649 simp only [finset.mem_bind, finset.singleton_eq_singleton, finset.mem_singleton] at this,
650 rcases this with ⟨a₁, h₁, a₂, h₂, rfl⟩,
651 rw [finsupp.to_multiset_add],
652 exact add_le_add (finset.le_sup h₁) (finset.le_sup h₂)
653 end
st └─┘
654
655 lemma degrees_prod {ι : Type*} (s : finset ι) (f : ι → mv_polynomial σ α) :
id └┘ ┴ ┴ ┴ ┴
src └┘
typ └┘ ┴ ┴ ┴ ┴
doc └┘
656 (s.prod f).degrees ≤ s.sum (λi, (f i).degrees) :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
657 begin
658 refine s.induction _ _,
659 { simp only [finset.prod_empty, finset.sum_empty, degrees_one] },
st └┘
660 { assume i s his ih,
661 rw [finset.prod_insert his, finset.sum_insert his],
662 exact le_trans (degrees_mul _ _) (add_le_add_left ih _) }
st └─
663 end
st ──┘
664
665 lemma degrees_pow (p : mv_polynomial σ α) :
id ┴ ┴
typ ┴ ┴
666 ∀(n : ℕ), (p^n).degrees ≤ add_monoid.smul n p.degrees
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
667 | 0 := begin rw [pow_zero, degrees_one], exact multiset.zero_le _ end
st └─┘
668 | (n + 1) := le_trans (degrees_mul _ _) (add_le_add_left (degrees_pow n) _)
id ┴
typ ┴
669
670 end comm_semiring
671
672 end degrees
673
674 section vars
675
676 /-- `vars p` is the set of variables appearing in the polynomial `p` -/
677 def vars (p : mv_polynomial σ α) : finset σ := p.degrees.to_finset
id ┴ ┴ ┴ └┘ ┴
src ┴ └┘
typ ┴ ┴ ┴ └┘ ┴
doc ┴ └┘
678
679 @[simp] lemma vars_0 : (0 : mv_polynomial σ α).vars = ∅ :=
id ┴ ┴
typ ┴ ┴
doc └──┘
680 by rw [vars, degrees_zero, multiset.to_finset_zero]
st ┴
681
682 @[simp] lemma vars_monomial (h : a ≠ 0) : (monomial s a).vars = s.support :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
doc └──┘
683 by rw [vars, degrees_monomial_eq _ _ h, finsupp.to_finset_to_multiset]
st ┴
684
685 @[simp] lemma vars_C : (C a : mv_polynomial σ α).vars = ∅ :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
doc └──┘
686 by rw [vars, degrees_C, multiset.to_finset_zero]
st ┴
687
688 @[simp] lemma vars_X (h : 0 ≠ (1 : α)) : (X n : mv_polynomial σ α).vars = {n} :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
doc └──┘
689 by rw [X, vars_monomial h.symm, finsupp.support_single_ne_zero zero_ne_one.symm]
st ┴
690
691 end vars
692
693 section degree_of
694
695 /-- `degree_of n p` gives the highest power of X_n that appears in `p` -/
696 def degree_of (n : σ) (p : mv_polynomial σ α) : ℕ := p.degrees.count n
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
697
698 end degree_of
699
700 section total_degree
701 /-- `total_degree p` gives the maximum |s| over the monomials X^s in `p` -/
702 def total_degree (p : mv_polynomial σ α) : ℕ := p.support.sup (λs, s.sum $ λn e, e)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
703
704 lemma total_degree_eq (p : mv_polynomial σ α) :
id ┴ ┴
typ ┴ ┴
705 p.total_degree = p.support.sup (λm, m.to_multiset.card) :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
706 begin
707 rw [total_degree],
708 congr, funext m,
709 exact (finsupp.card_to_multiset _).symm
710 end
st └─┘
711
712 lemma total_degree_le_degrees_card (p : mv_polynomial σ α) :
id ┴ ┴
typ ┴ ┴
713 p.total_degree ≤ p.degrees.card :=
id ┴ ┴
typ ┴ ┴
714 begin
715 rw [total_degree_eq],
716 exact finset.sup_le (assume s hs, multiset.card_le_of_le $ finset.le_sup hs)
id ┴
typ ┴
717 end
st └─┘
718
719 lemma total_degree_C (a : α) : (C a : mv_polynomial σ α).total_degree = 0 :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
720 nat.eq_zero_of_le_zero $ finset.sup_le $ assume n hn,
id ┴
typ ┴
721 have _ := finsupp.support_single_subset hn,
722 begin
723 rw [finset.singleton_eq_singleton, finset.mem_singleton] at this,
724 subst this,
725 exact le_refl _
726 end
st └─┘
727
728 lemma total_degree_zero : (0 : mv_polynomial σ α).total_degree = 0 :=
id ┴ ┴
typ ┴ ┴
729 by rw [← C_0]; exact total_degree_C (0 : α)
id ┴
typ ┴
730
731 lemma total_degree_one : (1 : mv_polynomial σ α).total_degree = 0 :=
id ┴ ┴
typ ┴ ┴
732 total_degree_C (1 : α)
id ┴
typ ┴
733
734 lemma total_degree_add (a b : mv_polynomial σ α) :
id ┴ ┴
typ ┴ ┴
735 (a + b).total_degree ≤ max a.total_degree b.total_degree :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
736 finset.sup_le $ assume n hn,
id ┴
typ ┴
737 have _ := finsupp.support_add hn,
738 begin
739 rw finset.mem_union at this,
740 cases this,
741 { exact le_max_left_of_le (finset.le_sup this) },
st └┘
742 { exact le_max_right_of_le (finset.le_sup this) }
st └┘
743 end
st └─┘
744
745 lemma total_degree_mul (a b : mv_polynomial σ α) :
id ┴ ┴
typ ┴ ┴
746 (a * b).total_degree ≤ a.total_degree + b.total_degree :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
747 finset.sup_le $ assume n hn,
id ┴
typ ┴
748 have _ := finsupp.support_mul a b hn,
id ┴
typ ┴
749 begin
750 simp only [finset.mem_bind, finset.mem_singleton, finset.singleton_eq_singleton] at this,
751 rcases this with ⟨a₁, h₁, a₂, h₂, rfl⟩,
752 rw [finsupp.sum_add_index],
753 { exact add_le_add (finset.le_sup h₁) (finset.le_sup h₂) },
st └┘
754 { assume a, refl },
st └┘
755 { assume a b₁ b₂, refl }
st └┘
756 end
st └─┘
757
758 lemma total_degree_list_prod :
759 ∀(s : list (mv_polynomial σ α)), s.prod.total_degree ≤ (s.map mv_polynomial.total_degree).sum
id ┴ ┴
typ ┴ ┴
760 | [] := by rw [@list.prod_nil (mv_polynomial σ α) _, total_degree_one]; refl
id └──┘
src └──┘
typ └──┘
doc └──┘
761 | (p :: ps) :=
762 begin
763 rw [@list.prod_cons (mv_polynomial σ α) _, list.map, list.sum_cons],
id ┴ ┴
typ ┴ ┴
764 exact le_trans (total_degree_mul _ _) (add_le_add_left (total_degree_list_prod ps) _)
765 end
st └─┘
766
767 lemma total_degree_multiset_prod (s : multiset (mv_polynomial σ α)) :
id ┴ ┴
typ ┴ ┴
768 s.prod.total_degree ≤ (s.map mv_polynomial.total_degree).sum :=
769 begin
770 refine quotient.induction_on s (assume l, _),
771 rw [multiset.quot_mk_to_coe, multiset.coe_prod, multiset.coe_map, multiset.coe_sum],
772 exact total_degree_list_prod l
773 end
st └─┘
774
775 lemma total_degree_finset_prod {ι : Type*}
776 (s : finset ι) (f : ι → mv_polynomial σ α) :
id └┘ ┴ ┴ ┴ ┴
src └┘
typ └┘ ┴ ┴ ┴ ┴
doc └┘
777 (s.prod f).total_degree ≤ s.sum (λi, (f i).total_degree) :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
778 begin
779 refine le_trans (total_degree_multiset_prod _) _,
780 rw [multiset.map_map],
781 refl
782 end
st └─┘
783
784 end total_degree
785
786 end comm_semiring
787
788 section comm_ring
789 variable [comm_ring α]
id └┘ └──┘
src └┘ └──┘
typ └┘ └──┘
790 variables {p q : mv_polynomial σ α}
791
792 instance : ring (mv_polynomial σ α) := finsupp.ring
id ┴ ┴
typ ┴ ┴
793 instance : comm_ring (mv_polynomial σ α) := finsupp.comm_ring
id ┴ ┴
typ ┴ ┴
794 instance : has_scalar α (mv_polynomial σ α) := finsupp.has_scalar
id ┴ ┴ ┴
typ ┴ ┴ ┴
795 instance : module α (mv_polynomial σ α) := finsupp.module _ α
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
796
797 instance C.is_ring_hom : is_ring_hom (C : α → mv_polynomial σ α) :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
798 by apply is_ring_hom.of_semiring
799
800 variables (σ a a')
801 lemma C_sub : (C (a - a') : mv_polynomial σ α) = C a - C a' := is_ring_hom.map_sub _
id ┴ └┘ ┴ ┴ ┴ └┘
typ ┴ └┘ ┴ ┴ ┴ └┘
802
803 @[simp] lemma C_neg : (C (-a) : mv_polynomial σ α) = -C a := is_ring_hom.map_neg _
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
doc └──┘
804
805 @[simp] lemma coeff_sub (m : σ →₀ ℕ) (p q : mv_polynomial σ α) :
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
doc └──┘
806 coeff m (p - q) = coeff m p - coeff m q := finsupp.sub_apply
id ┴ ┴ ┴
typ ┴ ┴ ┴
807
808 instance coeff.is_add_group_hom (m : σ →₀ ℕ) :
id ┴ ┴
src ┴
typ ┴ ┴
809 is_add_group_hom (coeff m : mv_polynomial σ α → α) :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
810 { map_add := coeff_add m }
id ┴
typ ┴
811
812 variables {σ} (p)
813 theorem C_mul' : mv_polynomial.C a * p = a • p :=
id ┴ ┴
typ ┴ ┴
814 begin
815 apply finsupp.induction p,
816 { exact (mul_zero $ mv_polynomial.C a).trans (@smul_zero α (mv_polynomial σ α) _ _ _ a).symm },
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └┘
817 intros p b f haf hb0 ih,
818 rw [mul_add, ih, @smul_add α (mv_polynomial σ α) _ _ _ a], congr' 1,
id ┴ ┴ ┴
typ ┴ ┴ ┴
819 rw [finsupp.mul_def, finsupp.smul_single, mv_polynomial.C, mv_polynomial.monomial],
820 rw [finsupp.sum_single_index, finsupp.sum_single_index, zero_add, smul_eq_mul],
821 { rw [mul_zero, finsupp.single_zero] },
st ┴ └┘
822 { rw finsupp.sum_single_index,
823 all_goals { rw [zero_mul, finsupp.single_zero] } }
st ┴ └───
824 end
st ──┘
825
826 lemma smul_eq_C_mul (p : mv_polynomial σ α) (a : α) : a • p = C a * p :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
827 begin
828 rw [← finsupp.sum_single p, @finsupp.smul_sum (σ →₀ ℕ) α α, finsupp.mul_sum],
829 refine finset.sum_congr rfl (assume n _, _),
id ┴
typ ┴
830 simp only [finsupp.smul_single],
831 exact C_mul_monomial.symm
832 end
st └─┘
833
834 @[simp] lemma smul_eval (x) (p : mv_polynomial σ α) (s) : (s • p).eval x = s * p.eval x :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
835 by rw [smul_eq_C_mul, eval_mul, eval_C]
st ┴
836
837 section degrees
838
839 lemma degrees_neg (p : mv_polynomial σ α) : (- p).degrees = p.degrees :=
id ┴ ┴
typ ┴ ┴
840 by rw [degrees, finsupp.support_neg]; refl
id └──┘
src └──┘
typ └──┘
doc └──┘
841
842 lemma degrees_sub (p q : mv_polynomial σ α) :
id ┴ ┴
typ ┴ ┴
843 (p - q).degrees ≤ p.degrees ⊔ q.degrees :=
844 le_trans (degrees_add p (-q)) $ by rw [degrees_neg]
845
846 end degrees
847
848 section eval₂
849
850 variables [comm_ring β]
id └──┘ └─┘
src └──┘ └─┘
typ └──┘ └─┘
851 variables (f : α → β) [is_ring_hom f] (g : σ → β)
852
853 instance eval₂.is_ring_hom : is_ring_hom (eval₂ f g) :=
id ┴ ┴
typ ┴ ┴
854 by apply is_ring_hom.of_semiring
855
856 lemma eval₂_sub : (p - q).eval₂ f g = p.eval₂ f g - q.eval₂ f g := is_ring_hom.map_sub _
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
857
858 @[simp] lemma eval₂_neg : (-p).eval₂ f g = -(p.eval₂ f g) := is_ring_hom.map_neg _
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
doc └──┘
859
860 lemma hom_C (f : mv_polynomial σ ℤ → β) [is_ring_hom f] (n : ℤ) : f (C n) = (n : β) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
861 congr_fun (int.eq_cast' (f ∘ C)) n
id ┴
typ ┴
862
863 /-- A ring homomorphism f : Z[X_1, X_2, ...] → R
864 is determined by the evaluations f(X_1), f(X_2), ... -/
865 @[simp] lemma eval₂_hom_X {α : Type u} (c : ℤ → β) [is_ring_hom c]
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
doc └──┘
866 (f : mv_polynomial α ℤ → β) [is_ring_hom f] (x : mv_polynomial α ℤ) :
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
867 eval₂ c (f ∘ X) x = f x :=
id ┴ ┴
typ ┴ ┴
868 mv_polynomial.induction_on x
id ┴
typ ┴
869 (λ n, by { rw [hom_C f, eval₂_C, int.eq_cast' c], refl })
id ┴ ┴
typ ┴ ┴
st └┘
870 (λ p q hp hq, by { rw [eval₂_add, hp, hq], exact (is_ring_hom.map_add f).symm })
id ┴ ┴
typ ┴ ┴
st └┘
871 (λ p n hp, by { rw [eval₂_mul, eval₂_X, hp], exact (is_ring_hom.map_mul f).symm })
id ┴ ┴
typ ┴ ┴
st └┘
872
873 /-- Ring homomorphisms out of integer polynomials on a type `σ` are the same as
874 functions out of the type `σ`, -/
875 def hom_equiv : (mv_polynomial σ ℤ →+* β) ≃ (σ → β) :=
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
876 { to_fun := λ f, ⇑f ∘ X,
877 inv_fun := λ f, ring_hom.of (eval₂ (λ n : ℤ, (n : β)) f),
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
878 left_inv := λ f, ring_hom.ext $ eval₂_hom_X _ _,
879 right_inv := λ f, funext $ λ x, by simp only [ring_hom.coe_of, function.comp_app, eval₂_X] }
id ┴ ┴
typ ┴ ┴
880
881 end eval₂
882
883 section eval
884
885 variables (f : σ → α)
886
887 instance eval.is_ring_hom : is_ring_hom (eval f) := eval₂.is_ring_hom _ _
id ┴
typ ┴
888
889 lemma eval_sub : (p - q).eval f = p.eval f - q.eval f := is_ring_hom.map_sub _
id ┴ ┴ ┴
typ ┴ ┴ ┴
890
891 @[simp] lemma eval_neg : (-p).eval f = -(p.eval f) := is_ring_hom.map_neg _
id ┴ ┴
typ ┴ ┴
doc └──┘
892
893 end eval
894
895 section map
896
897 variables [comm_ring β]
id ┴ └┘ └┘ ┴
src ┴ └┘ └┘ ┴
typ ┴ └┘ └┘ ┴
898 variables (f : α → β) [is_ring_hom f]
899
900 instance map.is_ring_hom : is_ring_hom (map f : mv_polynomial σ α → mv_polynomial σ β) :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
901 eval₂.is_ring_hom _ _
902
903 lemma map_sub : (p - q).map f = p.map f - q.map f := is_ring_hom.map_sub _
id ┴ ┴ ┴
typ ┴ ┴ ┴
904
905 @[simp] lemma map_neg : (-p).map f = -(p.map f) := is_ring_hom.map_neg _
id ┴ ┴
typ ┴ ┴
doc └──┘
906
907 end map
908
909 end comm_ring
910
911 section rename
912 variables {α} [comm_semiring α]
id └──┘ └──┘
src └──┘ └──┘
typ └──┘ └──┘
913
914 /-- Rename all the variables in a multivariable polynomial. -/
915 def rename (f : β → γ) : mv_polynomial β α → mv_polynomial γ α :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
916 eval₂ C (X ∘ f)
id ┴
typ ┴
917
918 instance rename.is_semiring_hom (f : β → γ) :
id ┴ ┴
typ ┴ ┴
919 is_semiring_hom (rename f : mv_polynomial β α → mv_polynomial γ α) :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
920 by unfold rename; apply_instance
id └────────────┘
src └────────────┘
typ └────────────┘
doc └────────────┘
921
922 @[simp] lemma rename_C (f : β → γ) (a : α) : rename f (C a) = C a :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
923 eval₂_C _ _ _
924
925 @[simp] lemma rename_X (f : β → γ) (b : β) : rename f (X b : mv_polynomial β α) = X (f b) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
926 eval₂_X _ _ _
927
928 @[simp] lemma rename_zero (f : β → γ) :
id ┴ ┴
typ ┴ ┴
doc └──┘
929 rename f (0 : mv_polynomial β α) = 0 :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
930 eval₂_zero _ _
931
932 @[simp] lemma rename_one (f : β → γ) :
id ┴
typ ┴
doc └──┘
933 rename f (1 : mv_polynomial β α) = 1 :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
934 eval₂_one _ _
935
936 @[simp] lemma rename_add (f : β → γ) (p q : mv_polynomial β α) :
id ┴ ┴ ┴
typ ┴ ┴ ┴
doc └──┘
937 rename f (p + q) = rename f p + rename f q :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
938 eval₂_add _ _
939
940 @[simp] lemma rename_sub {α} [comm_ring α]
id ┴ └┘ └┘ ┴ ┴
src ┴ └┘ └┘ ┴
typ ┴ └┘ └┘ ┴ ┴
doc └──┘
941 (f : β → γ) (p q : mv_polynomial β α) :
id ┴ ┴ ┴
typ ┴ ┴ ┴
942 rename f (p - q) = rename f p - rename f q :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
943 eval₂_sub _ _ _
944
945 @[simp] lemma rename_mul (f : β → γ) (p q : mv_polynomial β α) :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
doc └──┘
946 rename f (p * q) = rename f p * rename f q :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
947 eval₂_mul _ _
948
949 @[simp] lemma rename_pow (f : β → γ) (p : mv_polynomial β α) (n : ℕ) :
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
doc └──┘
950 rename f (p^n) = (rename f p)^n :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
951 eval₂_pow _ _
952
953 lemma map_rename [comm_semiring β] (f : α → β) [is_semiring_hom f]
id ┴ └┘ └┘ └┘ └┘ ┴ ┴ ┴ ┴
src ┴ └┘ └┘ └┘ └┘
typ ┴ └┘ └┘ └┘ └┘ ┴ ┴ ┴ ┴
954 (g : γ → δ) (p : mv_polynomial γ α) :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
955 map f (rename g p) = rename g (map f p) :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
956 mv_polynomial.induction_on p
id ┴
typ ┴
957 (λ a, by simp)
id ┴
typ ┴
958 (λ p q hp hq, by simp [hp, hq])
id ┴ ┴
typ ┴ ┴
959 (λ p n hp, by simp [hp])
id ┴ ┴
typ ┴ ┴
960
961 @[simp] lemma rename_rename (f : β → γ) (g : γ → δ) (p : mv_polynomial β α) :
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
962 rename g (rename f p) = rename (g ∘ f) p :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
963 show rename g (eval₂ C (X ∘ f) p) = _,
id ┴ ┴
typ ┴ ┴
964 by simp only [eval₂_comp_left (rename g) C (X ∘ f) p, (∘), rename_C, rename_X]; refl
id ┴ ┴ ┴ └──┘
src └──┘
typ ┴ ┴ ┴ └──┘
doc └──┘
965
966 @[simp] lemma rename_id (p : mv_polynomial β α) : rename id p = p :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
doc └──┘
967 eval₂_eta p
id ┴
typ ┴
968
969 lemma rename_monomial (f : β → γ) (p : β →₀ ℕ) (a : α) :
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
970 rename f (monomial p a) = monomial (p.map_domain f) a :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
971 begin
972 rw [rename, eval₂_monomial, monomial_eq, finsupp.prod_map_domain_index],
973 { exact assume n, pow_zero _ },
id ┴
typ ┴
st └┘
974 { exact assume n i₁ i₂, pow_add _ _ _ }
id ┴ └┘ └┘
typ ┴ └┘ └┘
st └─
975 end
st ──┘
976
977 lemma rename_eq (f : β → γ) (p : mv_polynomial β α) :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
978 rename f p = finsupp.map_domain (finsupp.map_domain f) p :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
979 begin
980 simp only [rename, eval₂, finsupp.map_domain],
981 congr, ext s a : 2,
982 rw [← monomial, monomial_eq, finsupp.prod_sum_index],
983 congr, ext n i : 2,
984 rw [finsupp.prod_single_index],
985 exact pow_zero _,
986 exact assume a, pow_zero _,
id ┴
typ ┴
987 exact assume a b c, pow_add _ _ _
id ┴ ┴ ┴
typ ┴ ┴ ┴
988 end
st └─┘
989
990 lemma injective_rename (f : β → γ) (hf : function.injective f) :
id ┴ ┴ ┴
typ ┴ ┴ ┴
991 function.injective (rename f : mv_polynomial β α → mv_polynomial γ α) :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
992 have (rename f : mv_polynomial β α → mv_polynomial γ α) =
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
993 finsupp.map_domain (finsupp.map_domain f) := funext (rename_eq f),
id ┴ ┴
typ ┴ ┴
994 begin
995 rw this,
996 exact finsupp.injective_map_domain (finsupp.injective_map_domain hf)
id └┘
typ └┘
997 end
st └─┘
998
999 lemma total_degree_rename_le (f : β → γ) (p : mv_polynomial β α) :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1000 (p.rename f).total_degree ≤ p.total_degree :=
id ┴ ┴
typ ┴ ┴
1001 finset.sup_le $ assume b,
1002 begin
1003 assume h,
1004 rw rename_eq at h,
1005 have h' := finsupp.map_domain_support h,
1006 rw finset.mem_image at h',
1007 rcases h' with ⟨s, hs, rfl⟩,
1008 rw finsupp.sum_map_domain_index,
1009 exact le_trans (le_refl _) (finset.le_sup hs),
1010 exact assume _, rfl,
id ┴
typ ┴
1011 exact assume _ _ _, rfl
id ┴ ┴ ┴
typ ┴ ┴ ┴
1012 end
st └─┘
1013
1014 section
1015 variables [comm_semiring β] (f : α → β) [is_semiring_hom f]
id └──┘ └──┘ ┴
src └──┘ └──┘ ┴
typ └──┘ └──┘ ┴
1016 variables (k : γ → δ) (g : δ → β) (p : mv_polynomial γ α)
1017
1018 lemma eval₂_rename : (p.rename k).eval₂ f g = p.eval₂ f (g ∘ k) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1019 by apply mv_polynomial.induction_on p; { intros, simp [*] }
st └┘
1020
1021 lemma rename_eval₂ (g : δ → mv_polynomial γ α) :
id ┴ ┴ ┴
typ ┴ ┴ ┴
1022 (p.eval₂ C (g ∘ k)).rename k = (p.rename k).eval₂ C (rename k ∘ g) :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
1023 by apply mv_polynomial.induction_on p; { intros, simp [*] }
st └┘
1024
1025 lemma rename_prodmk_eval₂ (d : δ) (g : γ → mv_polynomial γ α) :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1026 (p.eval₂ C g).rename (prod.mk d) = p.eval₂ C (λ x, (g x).rename (prod.mk d)) :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
1027 by apply mv_polynomial.induction_on p; { intros, simp [*] }
st └┘
1028
1029 lemma eval₂_rename_prodmk (g : δ × γ → β) (d : δ) :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1030 (rename (prod.mk d) p).eval₂ f g = eval₂ f (λ i, g (d, i)) p :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1031 by apply mv_polynomial.induction_on p; { intros, simp [*] }
st └┘
1032
1033 lemma eval_rename_prodmk (g : δ × γ → α) (d : δ) :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1034 (rename (prod.mk d) p).eval g = eval (λ i, g (d, i)) p :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
1035 eval₂_rename_prodmk id _ _ _
1036
1037 end
1038
1039 end rename
1040
1041 lemma eval₂_cast_comp {β : Type u} {γ : Type v} (f : γ → β)
id ┴ ┴
typ ┴ ┴
1042 {α : Type w} [comm_ring α] (c : ℤ → α) [is_ring_hom c] (g : β → α) (x : mv_polynomial γ ℤ) :
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1043 eval₂ c (g ∘ f) x = eval₂ c g (rename f x) :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
1044 mv_polynomial.induction_on x
id ┴
typ ┴
1045 (λ n, by simp only [eval₂_C, rename_C])
id ┴
typ ┴
1046 (λ p q hp hq, by simp only [hp, hq, rename, eval₂_add])
id ┴ ┴
typ ┴ ┴
1047 (λ p n hp, by simp only [hp, rename, eval₂_X, eval₂_mul])
id ┴ ┴
typ ┴ ┴
1048
1049 instance rename.is_ring_hom
1050 {α} [comm_ring α] (f : β → γ) :
id └──┘ └─┘ ┴ ┴
src └──┘ └─┘
typ └──┘ └─┘ ┴ ┴
1051 is_ring_hom (rename f : mv_polynomial β α → mv_polynomial γ α) :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
1052 @is_ring_hom.of_semiring (mv_polynomial β α) (mv_polynomial γ α) _ _ (rename f)
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
1053 (rename.is_semiring_hom f)
id ┴
typ ┴
1054
1055 section equiv
1056
1057 variables (α) [comm_semiring α]
id ┴ └┘ └┘ └┘ └┘
src ┴ └┘ └┘ └┘ └┘
typ ┴ └┘ └┘ └┘ └┘
1058
1059 /-- The ring isomorphism between multivariable polynomials in no variables and the ground ring. -/
1060 def pempty_ring_equiv : mv_polynomial pempty α ≃+* α :=
id └────┘ ┴ ┴
src └────┘
typ └────┘ ┴ ┴
doc └────┘
1061 { to_fun := mv_polynomial.eval₂ id $ pempty.elim,
1062 inv_fun := C,
1063 left_inv := is_id _ (by apply_instance) (assume a, by rw [eval₂_C]; refl) (assume a, a.elim),
id ┴ └──┘ ┴ ┴
src └──┘
typ ┴ └──┘ ┴ ┴
doc └──┘
1064 right_inv := λ r, eval₂_C _ _ _,
id ┴
typ ┴
1065 map_mul' := λ _ _, eval₂_mul _ _,
id ┴ ┴
typ ┴ ┴
1066 map_add' := λ _ _, eval₂_add _ _ }
id ┴
typ ┴
1067
1068 /--
1069 The ring isomorphism between multivariable polynomials in a single variable and
1070 polynomials over the ground ring.
1071 -/
1072 def punit_ring_equiv : mv_polynomial punit α ≃+* polynomial α :=
id └───┘ ┴ ┴
src └───┘
typ └───┘ ┴ ┴
1073 { to_fun := eval₂ polynomial.C (λu:punit, polynomial.X),
id └──┘
src └──┘
typ └──┘
1074 inv_fun := polynomial.eval₂ mv_polynomial.C (X punit.star),
id └──┘ └──┘
src └──┘ └──┘
typ └──┘ └──┘
1075 left_inv :=
1076 begin
1077 refine is_id _ _ _ _,
1078 apply is_semiring_hom.comp (eval₂ polynomial.C (λu:punit, polynomial.X)) _; apply_instance,
id └───┘ └────────────┘
src └───┘ └────────────┘
typ └───┘ └────────────┘
doc └────────────┘
1079 { assume a, rw [eval₂_C, polynomial.eval₂_C] },
st ┴ └┘
1080 { rintros ⟨⟩, rw [eval₂_X, polynomial.eval₂_X] }
st ┴ └┘
1081 end,
st └─┘
1082 right_inv := assume p, polynomial.induction_on p
id ┴ ┴
typ ┴ ┴
1083 (assume a, by rw [polynomial.eval₂_C, mv_polynomial.eval₂_C])
id ┴
typ ┴
st ┴
1084 (assume p q hp hq, by rw [polynomial.eval₂_add, mv_polynomial.eval₂_add, hp, hq])
id ┴ ┴
typ ┴ ┴
st ┴
1085 (assume p n hp,
id ┴ ┴
typ ┴ ┴
1086 by rw [polynomial.eval₂_mul, polynomial.eval₂_pow, polynomial.eval₂_X, polynomial.eval₂_C,
1087 eval₂_mul, eval₂_C, eval₂_pow, eval₂_X]),
st ┴
1088 map_mul' := λ _ _, eval₂_mul _ _,
id ┴ ┴
typ ┴ ┴
1089 map_add' := λ _ _, eval₂_add _ _ }
id ┴ ┴
typ ┴ ┴
1090
1091 /-- The ring isomorphism between multivariable polynomials induced by an equivalence of the variables. -/
1092 def ring_equiv_of_equiv (e : β ≃ γ) : mv_polynomial β α ≃+* mv_polynomial γ α :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
1093 { to_fun := rename e,
id ┴
typ ┴
1094 inv_fun := rename e.symm,
id ┴
typ ┴
1095 left_inv := λ p, by simp only [rename_rename, (∘), e.symm_apply_apply]; exact rename_id p,
id ┴
typ ┴
1096 right_inv := λ p, by simp only [rename_rename, (∘), e.apply_symm_apply]; exact rename_id p,
id ┴ ┴
typ ┴ ┴
1097 map_mul' := rename_mul e,
id ┴
typ ┴
1098 map_add' := rename_add e }
id ┴
typ ┴
1099
1100 /-- The ring isomorphism between multivariable polynomials induced by a ring isomorphism of the ground ring. -/
1101 def ring_equiv_congr [comm_semiring γ] (e : α ≃+* γ) : mv_polynomial β α ≃+* mv_polynomial β γ :=
id └┘ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ └──┘ └─┘
typ └┘ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
1102 { to_fun := map e,
1103 inv_fun := map e.symm,
1104 left_inv := assume p,
1105 have (e.symm ∘ e) = id,
1106 { ext a, exact e.symm_apply_apply a },
id ┴
typ ┴
st └┘
1107 by simp only [map_map, this, map_id],
1108 right_inv := assume p,
id ┴
typ ┴
1109 have (e ∘ e.symm) = id,
1110 { ext a, exact e.apply_symm_apply a },
id ┴
typ ┴
st └┘
1111 by simp only [map_map, this, map_id],
1112 map_mul' := map_mul _,
1113 map_add' := map_add _ }
1114
1115 section
1116 variables (β γ δ)
1117
1118 /--
1119 The function from multivariable polynomials in a sum of two types,
1120 to multivariable polynomials in one of the types,
1121 with coefficents in multivariable polynomials in the other type.
1122
1123 See `sum_ring_equiv` for the ring isomorphism.
1124 -/
1125 def sum_to_iter : mv_polynomial (β ⊕ γ) α → mv_polynomial β (mv_polynomial γ α) :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
1126 eval₂ (C ∘ C) (λbc, sum.rec_on bc X (C ∘ X))
id └┘ └┘
typ └┘ └┘
1127
1128 instance is_semiring_hom_C_C :
1129 is_semiring_hom (C ∘ C : α → mv_polynomial β (mv_polynomial γ α)) :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1130 @is_semiring_hom.comp _ _ _ _ C mv_polynomial.is_semiring_hom _ _ C mv_polynomial.is_semiring_hom
1131
1132 instance is_semiring_hom_sum_to_iter : is_semiring_hom (sum_to_iter α β γ) :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
1133 eval₂.is_semiring_hom _ _
1134
1135 lemma sum_to_iter_C (a : α) : sum_to_iter α β γ (C a) = C (C a) :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
1136 eval₂_C _ _ a
id ┴
typ ┴
1137
1138 lemma sum_to_iter_Xl (b : β) : sum_to_iter α β γ (X (sum.inl b)) = X b :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
1139 eval₂_X _ _ (sum.inl b)
id ┴
typ ┴
1140
1141 lemma sum_to_iter_Xr (c : γ) : sum_to_iter α β γ (X (sum.inr c)) = C (X c) :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
1142 eval₂_X _ _ (sum.inr c)
id ┴
typ ┴
1143
1144 /--
1145 The function from multivariable polynomials in one type,
1146 with coefficents in multivariable polynomials in another type,
1147 to multivariable polynomials in the sum of the two types.
1148
1149 See `sum_ring_equiv` for the ring isomorphism.
1150 -/
1151 def iter_to_sum : mv_polynomial β (mv_polynomial γ α) → mv_polynomial (β ⊕ γ) α :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
1152 eval₂ (eval₂ C (X ∘ sum.inr)) (X ∘ sum.inl)
1153
1154 instance is_semiring_hom_iter_to_sum : is_semiring_hom (iter_to_sum α β γ) :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
1155 eval₂.is_semiring_hom _ _
1156
1157 lemma iter_to_sum_C_C (a : α) : iter_to_sum α β γ (C (C a)) = C a :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
1158 eq.trans (eval₂_C _ _ (C a)) (eval₂_C _ _ _)
id ┴
typ ┴
1159
1160 lemma iter_to_sum_X (b : β) : iter_to_sum α β γ (X b) = X (sum.inl b) :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
1161 eval₂_X _ _ _
1162
1163 lemma iter_to_sum_C_X (c : γ) : iter_to_sum α β γ (C (X c)) = X (sum.inr c) :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
1164 eq.trans (eval₂_C _ _ (X c)) (eval₂_X _ _ _)
id ┴
typ ┴
1165
1166 /-- A helper function for `sum_ring_equiv`. -/
1167 def mv_polynomial_equiv_mv_polynomial [comm_semiring δ]
id ┴ └──┘ └──┘ ┴
src ┴ └──┘ └──┘
typ ┴ └──┘ └──┘ ┴
1168 (f : mv_polynomial β α → mv_polynomial γ δ) (hf : is_semiring_hom f)
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1169 (g : mv_polynomial γ δ → mv_polynomial β α) (hg : is_semiring_hom g)
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1170 (hfgC : ∀a, f (g (C a)) = C a)
id ┴ ┴ ┴
typ ┴ ┴ ┴
1171 (hfgX : ∀n, f (g (X n)) = X n)
id ┴ ┴ ┴
typ ┴ ┴ ┴
1172 (hgfC : ∀a, g (f (C a)) = C a)
id ┴ ┴ ┴
typ ┴ ┴ ┴
1173 (hgfX : ∀n, g (f (X n)) = X n) :
id ┴ ┴ ┴
typ ┴ ┴ ┴
1174 mv_polynomial β α ≃+* mv_polynomial γ δ :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1175 { to_fun := f, inv_fun := g,
1176 left_inv := is_id _ (is_semiring_hom.comp _ _) hgfC hgfX,
1177 right_inv := is_id _ (is_semiring_hom.comp _ _) hfgC hfgX,
1178 map_mul' := hf.map_mul,
1179 map_add' := hf.map_add }
1180
1181 /--
1182 The ring isomorphism between multivariable polynomials in a sum of two types,
1183 and multivariable polynomials in one of the types,
1184 with coefficents in multivariable polynomials in the other type.
1185 -/
1186 def sum_ring_equiv : mv_polynomial (β ⊕ γ) α ≃+* mv_polynomial β (mv_polynomial γ α) :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
1187 begin
1188 apply @mv_polynomial_equiv_mv_polynomial α (β ⊕ γ) _ _ _ _
1189 (sum_to_iter α β γ) _ (iter_to_sum α β γ) _,
1190 { assume p,
1191 apply hom_eq_hom _ _ _ _ _ _ p,
id ┴
typ ┴
1192 apply_instance,
1193 { apply @is_semiring_hom.comp _ _ _ _ _ _ _ _ _ _,
1194 apply_instance,
1195 apply @is_semiring_hom.comp _ _ _ _ _ _ _ _ _ _,
1196 apply_instance,
1197 { apply @mv_polynomial.is_semiring_hom },
st └┘
1198 { apply mv_polynomial.is_semiring_hom_iter_to_sum α β γ },
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └┘
1199 { apply mv_polynomial.is_semiring_hom_sum_to_iter α β γ } },
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └──┘
1200 { apply mv_polynomial.is_semiring_hom },
st └┘
1201 { assume a, rw [iter_to_sum_C_C α β γ, sum_to_iter_C α β γ] },
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
st ┴ └┘
1202 { assume c, rw [iter_to_sum_C_X α β γ, sum_to_iter_Xr α β γ] } },
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
st ┴ └──┘
1203 { assume b, rw [iter_to_sum_X α β γ, sum_to_iter_Xl α β γ] },
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
st ┴ └┘
1204 { assume a, rw [sum_to_iter_C α β γ, iter_to_sum_C_C α β γ] },
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
st ┴ └┘
1205 { assume n, cases n with b c,
id ┴
typ ┴
1206 { rw [sum_to_iter_Xl, iter_to_sum_X] },
st ┴ └┘
1207 { rw [sum_to_iter_Xr, iter_to_sum_C_X] } },
st ┴ └──┘
1208 { apply mv_polynomial.is_semiring_hom_sum_to_iter α β γ },
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └┘
1209 { apply mv_polynomial.is_semiring_hom_iter_to_sum α β γ }
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └─
1210 end
st ──┘
1211
1212 /--
1213 The ring isomorphism between multivariable polynomials in `option β` and
1214 polynomials with coefficients in `mv_polynomial β α`.
1215 -/
1216 def option_equiv_left : mv_polynomial (option β) α ≃+* polynomial (mv_polynomial β α) :=
id └┘ └┘ ┴ ┴ ┴ ┴
src └┘ └┘
typ └┘ └┘ ┴ ┴ ┴ ┴
1217 (ring_equiv_of_equiv α $ (equiv.option_equiv_sum_punit β).trans (equiv.sum_comm _ _)).trans $
id ┴ ┴
typ ┴ ┴
1218 (sum_ring_equiv α _ _).trans $
id ┴
typ ┴
1219 punit_ring_equiv _
1220
1221 /--
1222 The ring isomorphism between multivariable polynomials in `option β` and
1223 multivariable polynomials with coefficients in polynomials.
1224 -/
1225 def option_equiv_right : mv_polynomial (option β) α ≃+* mv_polynomial β (polynomial α) :=
id └┘ └┘ ┴ ┴ ┴ ┴
src └┘ └┘
typ └┘ └┘ ┴ ┴ ┴ ┴
1226 (ring_equiv_of_equiv α $ equiv.option_equiv_sum_punit.{0} β).trans $
id ┴ ┴
typ ┴ ┴
1227 (sum_ring_equiv α β unit).trans $
id ┴ ┴ └──┘
src └──┘
typ ┴ ┴ └──┘
doc └──┘
1228 ring_equiv_congr (mv_polynomial unit α) (punit_ring_equiv α)
id └──┘ ┴ ┴
src └──┘
typ └──┘ ┴ ┴
doc └──┘
1229
1230 end
1231
1232 end equiv
1233
1234 end mv_polynomial